Capture-avoiding substitutions

This section describes how capture-avoiding substitutions are implemented in mCRL2, using the data expression grammar from the data expressions section of the data library overview.

Substitutions

A substitution $\sigma$ is a function that maps variables to expressions. It is assumed that $\sigma$ has finite support, in other words there is a finite number of variables $v$ for which $\sigma(v) \neq v$ . We define the substitution update $\sigma[v := v']$ as follows:

$\sigma[v := v'](w) = \begin{cases} v' & \text{if } w = v \\ \sigma(w) & \text{otherwise} \end{cases}$

The capture avoiding substitution

Let $\sigma$ be a substitution that maps variables to data expressions, and let $x$ be an arbitrary data expression. Let $FV(x)$ be the free variables in $x$ , and let $FV(\sigma)$ be the free variables in the right-hand sides of $\sigma$ . More precisely,

$FV(\sigma) = \bigcup_{v \in \mathit{domain}(\sigma)} FV(\sigma(v)) \setminus \{v\}.$

We define a function $C$ that computes the capture-avoiding substitution $\sigma(x)$ using $C(x, \sigma, FV(x) \cup FV(\sigma))$ . The function $C$ is recursively defined as follows:

$\begin{array}{lll} C(v, \sigma, V) & = & \sigma(v) \\ C(f, \sigma, V) & = & f \\ C(x(x_1), \sigma, V) & = & C(x, \sigma, V)(C(x_1, \sigma, V)) \\[1ex] C(x\ \mathbf{whr}\ v = x_1, \sigma, V) & = & \begin{cases} C(x, \sigma, V \cup \{v\})\ \mathbf{whr}\ v = C(x_1, \sigma, V \cup \{v\}) & \text{if } \sigma(v) = v \text{ and } v \notin V \\ C(x, \sigma', V \cup \{v'\})\ \mathbf{whr}\ v' = C(x_1, \sigma', V \cup \{v'\}) & \text{otherwise} \end{cases} \\[4ex] C(\Lambda v.x, \sigma, V) & = & \begin{cases} \Lambda v.C(x, \sigma, V \cup \{v\}) & \text{if } \sigma(v) = v \text{ and } v \notin V \\ \Lambda v'.C(x, \sigma', V \cup \{v'\}) & \text{otherwise} \end{cases} \end{array}$

where $\Lambda \in \{\forall, \exists, \lambda\}$ , where $v'$ is an arbitrary variable such that $\sigma(v') = v'$ and $v' \notin V$ , and where $\sigma' = \sigma[v := v']$ .

Caution

The extension of $C$ to assignments given below is not correct and does not match the actual implementation.

The function $C$ can be extended to assignments as follows:

$\begin{array}{lll} C(v = x, \sigma, V) & = & \begin{cases} v = C(x, \sigma, V \cup \{v\}) & \text{if } \sigma(v) = v \text{ and } v \notin V \\ v' = C(x, \sigma', V \cup \{v'\}) & \text{otherwise} \end{cases} \end{array}$

Example

Let $x = \forall b{:}\mathbb{B}.\ b \Rightarrow \forall c{:}\mathbb{B}.\ c \Rightarrow d$ and let $\sigma = [d := b]$ . Then $C(x, \sigma, FV(x) \cup FV(\sigma)) = \forall b'{:}\mathbb{B}.\ b' \Rightarrow \forall c{:}\mathbb{B}.\ c \Rightarrow b$ .

Capture-avoiding substitutions with an identifier generator

Let $\sigma$ be a substitution that maps variables to data expressions. In this section a substitution is defined that is more efficient than the capture-avoiding substitution of the previous section because it does not require the calculation of a set $V$ of variables.

It does require that $\sigma$ can indicate efficiently whether a variable occurs in $\sigma(y)$ (with $\sigma(y) \neq y$ ) for some variable $y$ . Furthermore, it requires an identifier generator that can generate variable names that are guaranteed to be fresh in the sense that they do not occur in any term.

This substitution has been implemented as replace_variables_capture_avoiding_with_an_identifier_generator. We use $\mathit{FV}(x)$ , $\mathit{FV}(\sigma)$ and $\sigma[v := v']$ as defined in the previous section.

The substitution is defined as $\hat{C}$ that calculates $\sigma(x)$ using $\hat{C}(x, \sigma)$ recursively as follows:

$\begin{array}{lll} \hat{C}(v, \sigma) & = & \sigma(v) \\ \hat{C}(f, \sigma) & = & f \\ \hat{C}(x(x_1), \sigma) & = & \hat{C}(x, \sigma)(\hat{C}(x_1, \sigma)) \\[1ex] \hat{C}(x\ \mathbf{whr}\ v = x_1, \sigma) & = & \begin{cases} \hat{C}(x, \sigma[v := v])\ \mathbf{whr}\ v = \hat{C}(x_1, \sigma) & \text{if } v \notin \mathit{FV}(\sigma), \\ \hat{C}(x, \sigma[v := v'])\ \mathbf{whr}\ v' = \hat{C}(x_1, \sigma) & \text{otherwise.} \end{cases} \\[4ex] \hat{C}(\Lambda v.x, \sigma, V) & = & \begin{cases} \Lambda v.\hat{C}(x, \sigma[v := v]) & \text{if } v \notin \mathit{FV}(\sigma), \\ \Lambda v'.\hat{C}(x, \sigma', V \cup \{v'\}) & \text{otherwise,} \end{cases} \end{array}$

where $\Lambda \in \{\forall, \exists, \lambda\}$ , where $v'$ is a fresh variable such that $\sigma(v') = v'$ and $v' \notin \mathit{FV}(\sigma) \cup \mathit{FV}(x)$ . The identifier generator is used to generate the name for $v'$ .

In the examples below $[]$ is the substitution mapping each variable onto itself and $[w := v']$ is the substitution mapping all variables onto itself, except that $w$ is mapped to $v'$ .

Example

Let $x = \forall b{:}\mathbb{B}.\ b \Rightarrow \forall c{:}\mathbb{B}.\ c \Rightarrow d$ and let $\sigma = [d := b]$ . Then $\hat{C}(x, \sigma) = \forall b'{:}\mathbb{B}.\ b' \Rightarrow \forall c{:}\mathbb{B}.\ c \Rightarrow b$ where $b'$ is a fresh variable.

Example

It is necessary that $v'$ above is chosen such that $v' \notin \mathit{FV}(\sigma) \cup \mathit{FV}(x)$ . We provide two examples to show what goes wrong if this condition is not satisfied.

If $v' \notin \mathit{FV}(\sigma)$ is not required, the following is possible: $\hat{C}(\forall v.w,\ [w := v']) = \forall v'.\hat{C}(w,\ [w := v']) = \forall v'.v'$ .
If $v' \notin \mathit{FV}(x)$ is not required, it is possible that: $\hat{C}(\forall v.v',\ []) = \forall v'.\hat{C}(v',\ []) = \forall v'.v$ .

Example

In a where clause the substitutions applied to the equations after the where can remain unchanged. For example,

$\hat{C}(f(u,v)\ \mathbf{whr}\ v=v,\ [u:=v]) = \hat{C}(f(u,v),\ [u:=v,\ v:=v'])\ \mathbf{whr}\ v' = \hat{C}(v,\ [u:=v]) = f(v,v')\ \mathbf{whr}\ v'=v.$

In an expression $f(u, v)\ \mathbf{whr}\ v = v$ the variable $v$ at the left-hand side of the $=$ is a local variable, whereas the $v$ at the right-hand side is globally bound.