Programming Language Theory Concept

Capture-avoiding substitution

Books

Journey Statuslearning

[x \to s] λ y . t = {\begin{matrix} λ y . [x \to s] t & if y \neq x \land y \notin F V (s) \\ λ y . t & if y = x \end{matrix}

$[x \to s] (t_{1} t_{2}) = [x \to s] t_{1} [x \to s] t_{2}$
Practical foundations for programming languages 's notation
A substitution $[b / x]$ is a Partial function on the set of Abstract syntax tree (AST)s $𝒜$ . Given the set of variables $𝒳$ and an AST $a \in 𝒜$ :
- If $a = x \in 𝒳$ then $[b / x] a = b$ .
- If $a = y \in 𝒳$ and $y \neq x$ then $[b / x] y = y$ .
- $[b / x] o ({\vec{x}}_{1} . a_{1}; \dots; {\vec{x}}_{n} . a_{n}) = o ({\vec{x}}_{1} . a_{1}^{'}; \dots; {\vec{x}}_{n} . a_{n}^{'})$ , where for each $1 \leq i \leq n$ , we require that ${\vec{x}}_{i} \notin b$ , and we set $a_{i}^{'} = [b / x] a_{i}$ if $x \notin {\vec{x}}_{i}$ , and $a_{i}^{'} = a_{i}$ otherwise.