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.