utlc/lambda design

Design goal

utlc/lambda is the untyped lambda calculus written as directly as possible on top of the shared layers: named terms from syntax, capture-avoiding substitution from substitution, and a strategy from eval. It is meant to be obviously right rather than fast, so that faster normalizers (debruijn, utlc/nbe) and the typed calculus stlc can be checked against it.

Mathematical background

Lambda terms are $t ::= v \mid x \mid t\,u \mid \lambda x.\,t$ , encoded as Value, Variable, Apply(t, [u]) and Bind(x, t); an n-ary Apply(f, [a_1, …, a_n]) denotes the curried spine $f\,a_1 \cdots a_n$ . Terms are taken modulo $=_\alpha$ .

Beta and eta

\begin{aligned} (\beta)\quad & (\lambda x.\,b)\,a \;\to\; b[x := a], \\ (\eta)\quad & \lambda x.\,f\,x \;\to\; f \qquad \text{if } x \notin \mathrm{FV}(f). \end{aligned}

Both are closed under all contexts, including under $\lambda$ (the $\xi$ rule). The side condition of eta is essential: without it $\lambda x.\,x\,x \to x$ would turn a closed term into an open one and identify functions that behave differently. Eta expresses extensionality: in the presence of $\beta$ , it is equivalent to the rule “if $f\,x = g\,x$ for a fresh $x$ then $f = g$ ”, because

f \;\leftarrow_\eta\; \lambda x.\,f\,x \;=\; \lambda x.\,g\,x \;\to_\eta\; g \qquad (x \notin \mathrm{FV}(f) \cup \mathrm{FV}(g)).

Classical properties

Confluence. $\to_\beta$ and $\to_{\beta\eta}$ are Church–Rosser, so a term has at most one normal form up to $=_\alpha$ .¹1 Barendregt, The Lambda Calculus, Theorems 3.2.8 and 3.3.9.
Normalization. If a term has a beta normal form, the leftmost-outermost strategy reaches it (normalization theorem, see the eval design).
Eta postponement. Every $\beta\eta$ reduction can be rearranged so that all $\beta$ steps precede all $\eta$ steps; consequently a term has a $\beta\eta$ normal form iff it has a $\beta$ normal form.²2 Barendregt, The Lambda Calculus, §15.1.
Undecidability. Whether a term has a normal form is undecidable, which is why the normalizer takes a step limit.

Design decisions

Beta through the shared substitution

beta_rule calls Substitution::singleton(x, a).apply(b). All capture avoidance is therefore in one place, proved once in the substitution design. For the redex $(\lambda x.\,\lambda y.\,x\,y)\,y$ :

\begin{aligned} (\lambda x.\,\lambda y.\,x\,y)\,y &\to_\beta (\lambda y.\,x\,y)[x := y] \\ &= \lambda y_1.\,(x\,y_1)[x := y] && y \in \mathrm{FV}(\text{replacement}),\ \text{rename } y \\ &= \lambda y_1.\,y\,y_1 \\ &\to_\eta y . \end{aligned}

The substitution lemma (Barendregt 2.1.16, derived in the substitution design) is what makes beta well defined on alpha classes and compatible with contexts.

Spines are contracted one argument at a time

A redex is Apply(Bind(x, b), [a, ..rest]). It contracts with the first argument only and keeps the rest: $(\lambda x.\,b)\,a\,\bar r \to b[x := a]\,\bar r$ . This is beta on the curried reading of the spine, so every step is a single beta step and the step count equals the length of the corresponding curried reduction. The De Bruijn reducer makes the same choice, which keeps the two step by step comparable.

Eta only on unary applications

eta_rule matches Bind(x, Apply(f, [Variable(x)])). On the curried reading, $\lambda x.\,f\,a\,x$ (written Apply(f, [a, x])) is also an eta redex, but recognising it would require splitting the spine and rebuilding Apply(f, [a]). The rule stays syntactic; callers who build spines n-ary and need eta can normalize spines to unary form first.

Normal order with one combined rule

normalize runs beta_eta_rule with the NormalOrder strategy, so each step contracts the leftmost-outermost redex of either kind. The combined rule has one name, "beta_eta"; traces show positions but not which of the two rules fired. Because beta and eta redexes have different root constructors, the priority inside beta_eta_rule never changes the outcome of a step.

Correctness / invariants

beta_rule(t) = Some(u) implies $t \to_\beta u$ at the root; eta_rule likewise for $\eta$ , with the side condition checked by @syntax.free_variables.
normalize returns NormalForm(u, n) only for $u$ with no (unary) $\beta$ or $\eta$ redex anywhere (rewrite normal-form lemma).
By confluence, any two terminating runs of this package, of debruijn (beta only) or of utlc/nbe (beta only) on the same term give beta normal forms that are alpha-equivalent after conversion and spine flattening. The test “named and debruijn beta reduction agree modulo alpha” checks a step that requires renaming.
With beta and eta combined, normal order is used as the strategy; that it reaches the $\beta\eta$ normal form of every normalizing term rests on the normalization theorem for beta and eta postponement, and is checked by tests rather than proved here.

Alternatives rejected

A separate lambda AST. Using Term[T] keeps the calculus inside the shared substrate: the same analyses, substitution and traces apply, and domain values ride along unchanged.
Separate beta and eta normalizers. Offered indirectly: pass beta_rule or eta_rule to @eval.evaluate with any strategy.
Iterated substitution in beta. Beta substitutes once; the argument is not re-substituted, as the calculus requires.

Boundaries

No types: ill-behaved terms such as $\Omega$ are accepted and end with StepLimitReached.
No sharing: a duplicated argument is reduced once per copy. Use utlc/nbe for efficient normalization.
Eta recognises unary applications only.
Constants (Value) have no reduction rules here; add domain rules with rewrite or eval.

Barendregt, The Lambda Calculus, Theorems 3.2.8 and 3.3.9. ↩
Barendregt, The Lambda Calculus, §15.1. ↩