Substitution relation

It is a relation between 4 sets.

`.[. <- .].`
 1 2    3 4
  1. The expression
  2. The free name
  3. The binding expression
  4. The resultant expression
(x*x) [x <- 4] (4 * 4)

Basic examples

------------ for any name v
v[v <- E1]E1

------------ for any name x != v
x[v <- E1]x

unary function application

E1[v <- E]E1'  E2[v <- E]E2'
----------------------------
E1(E2)[v <- E]E1' (E2')

unary function declaration

We cannot substitute symbols of a function, without application.

----------------------------
v => { S } |v <- E1| v => { S }

For instance:

x => {
  let y = 1;
  y => y + 1
}

Does not get transformed into: x => { 1 => 1 + 1 }

On the other hand, within the function body itself, we can have transformations, if there are free variables there, which are not bound by the function head.

S[v <- E1]S'  x != v  E1 >< X1  x ∉ X1
--------------------------------------
x => { S } [v <- E1] x => {S'}
logo