THE EXPLICIT SUBSTITUTION substitution is not an atom — make it a first-class, step-by-step operation
In the textbook lambda calculus, substitution — replace x with a value throughout a term — is a single meta-level atom, assumed to happen instantly. Real machines cannot afford that: substituting into a large term is expensive, and doing it eagerly is wasteful. Explicit substitution (the λσ-calculus) makes substitution a syntactic construct with its own reduction rules, so it can be delayed, composed, and performed incrementally — pushed inward one step at a time, only where needed. Abadi, Cardelli, Curien & Lévy closed the gap between the calculus's atomic substitution and how an actual machine (environments, closures) implements it.
THE TECHNIQUE substitution [x:=v] as a delayed, step-by-step syntactic operation
Applying the substitution [x := 5] to x + 3 as an explicit machine step. The demo performs the substitution and evaluates: live demo
HISTORY & CREDIT Abadi, Cardelli, Curien & Lévy, 1990
“Substitution just happens.” — on a real machine it is work, and doing it atomically is a fiction. Explicit substitution makes it a construct with rules, so it can be delayed and shared — which is exactly what environments and closures already do. cited
1990 · Abadi, Cardelli, Curien & Lévy — “Explicit Substitutions” (POPL): the λσ-calculus, substitution as first-class syntax. lineage · bridges the atomic substitution of the λ-calculus and the environments of real machines (SECD, CEK). now · the theory behind efficient substitution in proof assistants and abstract machines.
Turn substitution into syntax with rules and it can wait, compose, and happen only where needed — which is all an environment ever was. The atom, made into a mechanism. Abadi-Cardelli-Curien-Lévy 1990
RECOMMEND FOR I-13 one substitution step, computed
On the canonical compiler, performing [x := 5] in x + 3 is a single explicit step to 8:
$ i13 run m_explicitsub.i13 # [x:=5] in x+3
RUN OK . 11 step(s) . peak stack 2 . call depth 1
result = 8
subst_steps = 1
Recommend: i13 sides with explicit substitution in practice, without the calculus. It never substitutes into a term at all — it binds an argument to a parameter and looks it up when needed (an environment, which is exactly what explicit substitution reveals substitution “really” is). So i13's def f(I x){...} applied to 5 does the [x:=5] as a lookup, one step, only where x occurs — the delayed, incremental substitution the λσ-calculus formalizes. Abadi et al. proved the atom was always a mechanism; i13, like every real machine, only ever implemented the mechanism.