substitution

The syntax is

e ::= x | λx.e | e e

free variables

FV(e) - Free variables of expression e.

FV(x) = {x}
FV(e₁ e₂) = FV(e₁) ∪ FV(e₂)
FV(λx.e) = FV(e) - {x}

examples

FV(λx.x) = {}
FV(x y) = FV(x) ∪ FV(y) = {x, y}
FV(λy.λx. x y) = {}

free variables just like global varibles in C programming language.

substitution

λx.e e₁ - when β reduction

[e₁|x]e - means locate x in e, and then substitute x with e₁ 1. e=x [e₁|x]x=e₁ 2. e=y y≠x [e₁|x]y=y 3. [e|x]e₁ e₂ = [e|x]e₁ [e|x]e₂ 4. [e|x]λy.e = ???

case 1, 2, 3 is easy

The last case

1st property of bound variable

λx. ... "rename" "x" name of this bound variable

λx.x ≡ₐ λy.y λx.λy.x y ≡ₐ λy.λx.y x ≡ₐ - α equivalance or α conversion

[e'|x]λx.e = λx.e - we can rename x to other variable, the substitution has no effects.

2nd property of bound variable [e'|x]e = (_) if z ∈ FV(e'), z will be still free after substitution. [e'|x]λy.e = where x≠y λy.[e'|x]e if y∈FV(e'), after substitution, something bad happens, y has been bound.

example: (λx.(λy.x)) y [y|x]λy.x = λy.[y|x]x = λy.y - y been bound!

we should rename y, maybe z. (λx.(λz.x)) y = [y|z]λz.x = λz.y - y still free.

this is called variable capture

we need capture avoiding substitution

[e'|x]λy.e = λz.[e'|x] e

"rename y to z"

if z∈FV(e), suppose we have e=z, FV(e) = {z} λy.z -> λz.z - z is bound

[e'|x]λy.e = λz.[e'|x][y⟷z]e