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.