The lambda calculus
This chapter builds an equational theory of the untyped lambda calculus with unary numerals. It extends the theory used in evaluation examples during the Proof search and Computation chapters. We end with the characteristic equation of the Y combinator.
Syntax
The sort tm contains terms. Its @vars pool supplies variables when a
proof needs them. Abstractions are λ x. e, applications are f · a, and
explicit substitution is [x := a] e, governed by the reduction rules
below. The numerals are unary (0, S0, SS0, with S in the delimiter
set so the compact form parses), and + is their addition.
The equational layer
The only judgments are term equations a = b and their iff equivalences,
bundled as in the Equality and normalization
chapter:
Note lam_congr: it lets an equation proved about a body a, possibly
mentioning the bound variable, lift to an equation between abstractions. This
is necessary to let rewriting descend under binders.
Reduction
Dependency restrictions prevent variable capture. In sb_lam, the
declaration (a: tm x) permits a to mention x but not y. Moving a
under the binder for y therefore cannot capture a variable in a.
The substitution rules carry two annotations. @rewrite lets the compiler run
substitutions whenever it checks an ordinary line, so a cited rule whose
conclusion contains a substitution can be stated in reduced form. @compute
enrolls the same equations, plus beta and the addition table, as directed
computation rules for conversion? (see Computation).
Single steps
@rewrite normalization alone is enough to make one beta step a one-line
proof. The right-hand side of beta’s instantiated conclusion is [x := 0] (S x). The line states the reduced form, and the compiler emits the
conversion:
For anything longer than one step, equations are chained by hand with the congruence and transitivity axioms. Here is the K combinator discarding its second argument:
l1 reduces under the binder through sb_lam (legal, since a doesn’t
mention y), and l4 discharges [y := b] a by sb_vac. Both capture facts
come straight from the binder declarations of the theorem.
Evaluation
A Church numeral represents a number by repeated function application. The
numeral for two applies its function twice. Giving it the successor function
and 0 therefore produces S S 0:
The goal is an equation, so conversion? only has to join its two sides: the
fold reduces the left side to S S 0. Church addition works the same way:
plus uses its first numeral to iterate f on top of the second’s result, and
1 + 1 = 2 is just evaluation.
The accepted suggestion expands to a long proof because every conversion step is emitted explicitly.
The Y combinator
The fixed-point combinator Y = λ f. (λ x. f · (x · x)) · (λ x. f · (x · x))
satisfies Y · g = g · (Y · g) for any g. Name it with a definition, whose
bound variables become dummy binders:
Writing ω for λ u. g · (u · u), one beta step takes Y · g to ω · ω,
and one more takes ω · ω to g · (ω · ω), so both sides of the fixed-point
equation reduce to a common term.
On l1, the function being applied is Y, not a visible abstraction. The
compiler unfolds Y to find the β-reduction step.
conversion? can find this equation, but only when the definition of Y is
used rather than the defined term Y. Only annotated definitions take part in
conversion, and a definition with hidden dummy binders can be folded but never
unfolded during conversion (see Computation), so Y is
opaque to that search method.