# 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'}