Explicit substitutions in lambda calculus

The beta reduction is known to contain substitution within one step, meaning that the reduction of $(\lambda x.M)N$ will be equivalent to the replacement of all free variables $x$ in $M$ by $N$, without capturing any variables. An interpreter will have to choose how to perform that replacement when the argument occurs multiple times or under another binding operation. In explicit substitution, the pending substitution becomes part of the term, thus making the operation visible to the reduction relation. This approach is introduced in Explicit Substitutions by Abadi, Cardelli, Curien, and Lévy.

Representation

Employ de Bruijn indices beginning from 0, where 0 denotes the closest binder, and 1 denotes the next binder after it. The index greater than the closest binders is used to refer to a position outside of the binders, and hence the example can have a free variable without introducing another constructor for a variable. $M[s]$ denotes a term with pending substitutions. After performing a beta reduction, we obtain $M[N/]$, where $N/$ substitutes index 0 with $N$ and decreases other indices since the term loses a binder:

type term =
  | Var of int
  | Lam of term
  | App of term * term
  | Susp of term * substitution
and substitution =
  | Replace of term
  | Shift
  | Lift of substitution

Crossing a binder

Substitution within an application has the two children performing the same pending operation; abstraction on the other hand requires the introduction of a variable which the operation should preserve. An abstraction on a lifting operation leaves its newly introduced index at zero while shifting the elements returned from previous indices by one position to the left. The shifting only applies to free variables when the abstraction is encountered because the variables bound within the argument substitution have to be preserved as originally referenced:

let rec lookup substitution index =
  match substitution, index with
  | Replace argument, 0 -> argument
  | Replace _, n -> Var (n - 1)
  | Shift, n -> Var (n + 1)
  | Lift _, 0 -> Var 0
  | Lift substitution, n -> Susp (lookup substitution (n - 1), Shift)

The term $(\lambda.\lambda.1)\;0$ is an example where the failure occurs. In this case, the argument is a free variable; hence the reduction must give us $\lambda.1$. The reduction must not produce $\lambda.0$ since that would mean capturing the argument and changing the constant function to the identity function:

Checking the steps

Examine each suspension via capture-avoiding substitution according to the ordinary procedure, resulting in an erasure to ordinary lambda terms. The condition of verification is that both propagation and lookup preserve erasure, while a single beta step is analogous to the ordinary beta reduction. Checking the relation on examples helps spot erroneous lifting but doesn’t prove confluence and termination for the extended calculus. This representation also provides no guarantee of any automatic sharing, because the application rule may introduce duplication of pending substitutions.

Demo

The demo proceeds according to the same rules, employing an outermost and left-first reduction that also takes place under abstractions. λ.0 and \.0 are identity; enter your terms with parentheses for grouping applications. Every step presents the rule applied and the set of pending substitutions, with a fixed step count to keep diverging terms inspectable. The OCaml reducer uses the entire traversal used by the examples.

Example Avoiding capture Distributing a substitution A bound argument Self application Term

Indices start at zero. N/ replaces index zero, ↑ shifts free indices and lift(s) crosses one binder.

Step Run up to 100 steps Reset

Loading the reducer.