Explicit Substitutions, or Substitutions If You Need to Implement Them

As I told you before, performance is something desirable when programming a λ interpreter. The sustitutions we saw are made in one step.

I will note the beta step as →β and a substitution step as →. For instance,

(λx.x) z  →β  x[x/z]  →  z.

The computations of the traditional lambda calculus are always:

T →β T' → → → → until no more substitutions can be made →β T'' → → →...

Now, if we want to control the substitutions, one can make some computations like

T →β T' few steps of sustitutions →β T'' →β T''...

To make it clear, supose the term

(λx. y) ((λx. x x) z)

One posible reduction in the traditional λ calculus is

(λx. y) ((λx. x x) z)  →β  (λx. y) (x x)[x/z]  →  (λx. y) (x[x/z] x[x/z])  →  (λx. y) (z x[x/z])  →  (λx. y) (z z)  →  y[x/(z z)]  →  y

But a more clever path is posible, if we don't make all the substitutions:

(λx. y) ((λx. x x) z)  →β  (λx. y) (x x)[x/z]  →  y[x/(x x)[x/z]]  →  y

So a calculus with explicit substitution is a calculus that has the substitutions as another rewriting rules. For instance, λx is the simpler calculus:

(λx. M) N
→β
M[x/N]


x[x/R]
→
R


y[x/R]
→
y


(T T’)[x/R]
→
T[x/R] T’[x/R]


(λy.T)[x/R]
→
(λy.T[x/R])

That's the idea behind explicit substitutions. It's very simple and yet has many issues I will show in future posts.