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]|
|(T T’)[x/R]||→||T[x/R] 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.