Ctrl+K

Curiosities and lore

Curiosities and lore#

Every field has its campfire stories. The λ-calculus — ninety years old, seven symbols deep — has better ones than most: a theorem discovered in a dentist’s chair, a single term that is simultaneously a number and a lie, an equation whose only honest answer is I don’t know. This chapter collects the folklore, and — because this is the Lambda Lab cookbook — every runnable claim in it has been run. Open the lab in a second tab and check us at every step; the outputs printed below are the engine’s own, verbatim.

The predecessor legend#

Princeton, early 1930s. Alonzo Church has his numerals: \(n\) is the act of doing something \(n\) times, \(\lambda f x.\, f^n(x)\). Addition, multiplication, even exponentiation fall out almost for free — to add, iterate the successor; to multiply, iterate the addition. Then someone asks the innocent question: what about subtracting one?

Suddenly everything is stuck. A numeral only knows how to apply \(f\) another time. There is no un-apply. From inside \(f^n(x)\) you cannot peel off a single \(f\) — the term offers you iteration and nothing else. Church, so the story goes, began to suspect that the predecessor function simply was not λ-definable, which would have been fatal for the whole enterprise of encoding arithmetic.

His student Stephen Kleene found the trick, and the anecdote — told by Kleene himself in his recollections (Origins of Recursive Function Theory, 1981) and lovingly retold ever since — is that the idea came to him in the dentist’s chair, while his wisdom teeth were being extracted. Take the story with the usual grain of salt reserved for well-polished anecdotes; the mathematics, however, checks out completely, as we are about to verify.

The insight: don’t undo — redo. If you cannot step backwards from \(n\), walk forwards from \(0\) and keep a one-step memory. Iterate, \(n\) times, the pair operation

\[ (a, b) \;\longmapsto\; (b,\, b+1) \]

starting from \((0,0)\). After \(n\) iterations the pair is \((n-1,\, n)\) — the second component counts the laps, the first trails one lap behind. Take the first component and you have subtracted one, using nothing but forward iteration.

Watch it happen. Start with let SHIFT = \p. PAIR (SND p) (SUCC (SND p)) and continue in the same session:

nf SND (SHIFT (PAIR 0 0))
nf 3 SHIFT (PAIR 0 0)
let KPRED = \n. FST (n SHIFT (PAIR 0 0))
nf KPRED 4
nf KPRED 0
equiv KPRED 7 = PRED 7

The lab answers, in order — one shift puts \(1\) in the back seat; three shifts (note the numeral 3 driving the loop) produce the pair \(\langle 2, 3\rangle\) in the flesh:

β-normal form · 16 step(s)
  λf x. f x
  = 1  (Church numeral)

β-normal form · 60 step(s)
  λf. f (λf' x. f' (f' x)) (λf'' x'. f'' (f'' (f'' x')))

and the assembled predecessor works, including at the famous edge case \(0 - 1 = 0\):

β-normal form · 46 step(s)
  λf x. f (f (f x))
  = 3  (Church numeral)

β-normal form · 9 step(s)
  λf x. x
  = 0 / FALSE  (the same untyped Church term)

β-convertibility by normal forms (η is not used)
  left NF:  λf x. f (f (f (f (f (f x)))))
  right NF: λf x. f (f (f (f (f (f x)))))
  equal β-normal forms up to α

The lab’s built-in PRED is a distilled one-liner of the same idea — the “pair” has been compiled away into two continuation-like arguments, but the trailing-memory trick is intact. Its trace is short enough to savour whole: run reduce PRED 2 and watch nine steps of 1930s dental surgery:

β-reduction (normal order · highlight = next redex)
  start:  (λn. (λf. (λx. n (λg. (λh. h (g f))) (λu. x) (λu'. u')))) (λf'. (λx'. f' (f' x')))
  →β      λf. (λx. (λf'. (λx'. f' (f' x'))) (λg. (λh. h (g f))) (λu. x) (λu'. u'))
  →β      λf. (λx. (λx'. (λg. (λh. h (g f))) ((λg'. (λh'. h' (g' f))) x')) (λu. x) (λu'. u'))
  →β      λf. (λx. (λg. (λh. h (g f))) ((λg'. (λh'. h' (g' f))) (λu. x)) (λu'. u'))
  →β      λf. (λx. (λh. h ((λg. (λh'. h' (g f))) (λu. x) f)) (λu'. u'))
  →β      λf. (λx. (λu. u) ((λg. (λh. h (g f))) (λu'. x) f))
  →β      λf. (λx. (λg. (λh. h (g f))) (λu. x) f)
  →β      λf. (λx. (λh. h ((λu. x) f)) f)
  →β      λf. (λx. f ((λu. x) f))
  →β      λf x. f x
  β-normal form reached in 9 step(s).
  = 1  (Church numeral)

Inspect the legend up close

The lab knows this is the famous one.

  • church PRED — the conceptual and fully-expanded forms of the “hard one”, side by side.

  • nf PRED 3 — the headline act in 11 steps: λf x. f (f x) = 2  (Church numeral).

  • debruijn PRED — the wisdom-tooth term namelessly: λ λ λ 2 (λ λ 0 (1 3)) (λ 1) (λ 0).

One term, two meanings: FALSE is 0#

Run decode FALSE and the lab refuses to pick a side:

  = 0 / FALSE  (the same untyped Church term)

This is not an implementation quirk. Look at the two definitions namelessly (debruijn FALSE, debruijn 0):

  named:    λt f. f
  nameless: λ λ 0

  named:    λf x. x
  nameless: λ λ 0

Identical. FALSE says take two things, return the second; the numeral 0 says take a function and an argument, apply the function zero times — which is to say, return the second thing. Same term, and equiv FALSE = 0 confirms it officially (equal β-normal forms up to α). The untyped λ-calculus has no opinion about what a term means; meaning is supplied entirely by the context that consumes it. Feed the term to a conditional and it selects the else-branch; feed it a successor and a number and it iterates zero times:

nf FALSE SUCC 2

β-normal form · 2 step(s)
  λf x. f (f x)
  = 2  (Church numeral)

FALSE just added zero. (Its partner in crime appears later in this chapter: when you define the K combinator, the lab dryly notes = TRUE  (Church boolean).)

How would types tell them apart? Ask ch term \t f. f: the principal type is α → β → β. The Boolean reading specializes it to \(o \to o \to o\); the numeral reading specializes it to \((\iota\to\iota) \to \iota \to \iota\). Both are instances of one scheme — but in a typed language you must declare which instance you mean, and Bool and Nat are different types by fiat. Typing is exactly the act of choosing one meaning and making the other one ill-formed. Untyped λ-calculus declines to choose, and this little pun is the cheapest demonstration of what that costs — and what it buys.

The η-story of exponent zero#

Here is a definition so elegant it appears in half the textbooks: exponentiation is

\[ \mathrm{POW} \;=\; \lambda m\, n.\; n\; m \]

— to compute \(m^n\), apply the numeral \(n\) to the numeral \(m\): iterating “compose with \(m\)” \(n\) times really does build \(m^n\). Try it: let NPOW = \m n. n m, then in the same session:

nf NPOW 2 3
nf NPOW 5 0
equiv NPOW 5 0 = 1

β-normal form · 16 step(s)
  λx x0. x (x (x (x (x (x (x (x x0)))))))
  = 8  (Church numeral)

\(2^3 = 8\): flawless. But now the second answer:

β-normal form · 3 step(s)
  λx. x

No (Church numeral) tag. \(5^0\) came out as the identity function — one λ short of the numeral 1 \(= \lambda f x.\, f\, x\). And the lab is strict about it:

β-convertibility by normal forms (η is not used)
  left NF:  λx. x
  right NF: λf x. f x
  different β-normal forms

Is the textbook wrong? Not quite — it is implicitly working modulo η: the principle that \(\lambda x.\, f\, x = f\) whenever \(x\) is not free in \(f\), i.e. that two functions agreeing on every argument are equal. Under η, the identity and the numeral 1 collapse into each other. Run eta 1 and watch extensionality act:

η-reduction  (λx. f x → f when x ∉ FV(f); no β steps taken)
  start:  λf x. f x
  →η      λf. f
  η-normal form reached in 1 step(s).

The lab keeps β and η deliberately separate — nf means exactly β-normal form, never a silent mix — so its built-in POW takes the other exit: it is η-expanded just enough that pure β suffices. Compare church POW: the definition is λm n f x. n m f x — the naive n m wearing two extra abstractions — and now nf POW 5 0 lands exactly on the canonical numeral:

β-normal form · 4 step(s)
  λf x. f x
  = 1  (Church numeral)

A one-character-deep moral: how equal you want your functions to be is a design decision, and \(m^0\) is where the decision becomes visible.

The Ω zoo#

Every calculus needs a monster. The classic is

\[ \Omega \;=\; (\lambda x.\, x\, x)\,(\lambda x.\, x\, x), \]

the self-application applied to itself. β-reduce it and the redex reproduces itself exactly: run reduce OMEGA:

β-reduction (normal order · highlight = next redex)
  start:  (λx. x x) (λx'. x' x')
  →β      (λx. x x) (λx'. x' x')
  →β      (λx. x x) (λx'. x' x')
  →β      (λx. x x) (λx'. x' x')
  ⋮
  … stopped after 60 steps; the displayed term is partial.

Sixty identical lines: Ω is a fixed point of β-reduction itself, running in place forever at constant size. It is the standard witness that not every term has a normal form — and, via ch term \x. x x, the standard witness of what simple types forbid to buy their termination theorem:

Term not typeable in STLC: Cannot unify α with α → β

But Ω loops politely. Add one more x and you get its feral cousin:

let OMEGA3 = (\x. x x x) (\x. x x x)
reduce OMEGA3

β-reduction (normal order · highlight = next redex)
  start:  (λx. x x x) (λx'. x' x' x')
  →β      (λx. x x x) (λx'. x' x' x') (λx''. x'' x'' x'')
  →β      (λx. x x x) (λx'. x' x' x') (λx''. x'' x'' x'') (λx'''. x''' x''' x''')
  →β      (λx. x x x) (λx'. x' x' x') (λx''. x'' x'' x'') (λx'''. x''' x''' x''') (λx'''2. x'''2 x'''2 x'''2)
  ⋮
  … stopped after 60 steps; the displayed term is partial.

Each step rewrites the head redex \((\lambda x.\, x\,x\,x)\,A\) into \(A\,A\,A\) — one copy of the triplicator in, three out — so the term gains a copy per step and its size increases strictly monotonically: a computation that not only never finishes but never even revisits a previous size. (Try nf OMEGA3 if you enjoy watching a step-limit report whose “partial term” is a paragraph wide.) Ω and Ω₃ bracket the two ways to diverge: in place, and explosively. And notice what nf OMEGA actually prints:

Reduction limit reached after 1000 β-step(s)
  Step limit reached. This is not claimed to be a normal form:
  (λx. x x) (λx'. x' x')

Not claimed to be a normal form. Hold that phrase — it becomes a theorem at the end of the chapter.

Fixed points of everything#

The fixed-point combinator (church Y shows λf. (λx. f (x x)) (λx. f (x x))) delivers on an outrageous promise: every term \(F\), without exception, has a fixed point, and \(Y\,F\) is one. The two-line proof is best watched live with a free variable standing in for an arbitrary \(F\) — run reduce Y g:

β-reduction (normal order · highlight = next redex)
  start:  (λf. (λx. f (x x)) (λx'. f (x' x'))) g
  →β      (λx. g (x x)) (λx'. g (x' x'))
  →β      g ((λx. g (x x)) (λx'. g (x' x')))
  →β      g (g ((λx. g (x x)) (λx'. g (x' x'))))
  →β      g (g (g ((λx. g (x x)) (λx'. g (x' x')))))
  ⋮
  … stopped after 60 steps; the displayed term is partial.

Line 2 to line 3 is the whole theorem: the term reached after one step reduces to g applied to itself, so \(Y g =_\beta g\,(Y g)\) — and then, having nothing better to do, it keeps unfolding, sprouting one more g per step, forever.

Because every term qualifies, we can demand fixed points of things that have no business having them. A fixed point of TRUE? TRUE ignores its second argument and returns its first, so its fixed point must be a function that swallows an argument and returns itself. Run reduce Y TRUE:

β-reduction (normal order · highlight = next redex)
  start:  (λf. (λx. f (x x)) (λx'. f (x' x'))) (λt. (λf'. t))
  →β      (λx. (λt. (λf. t)) (x x)) (λx'. (λt'. (λf'. t')) (x' x'))
  →β      (λt. (λf. t)) ((λx. (λt'. (λf'. t')) (x x)) (λx'. (λt''. (λf''. t'')) (x' x')))
  →β      λf. (λx. (λt. (λf'. t)) (x x)) (λx'. (λt'. (λf''. t')) (x' x'))
  ⋮
  →β      λf. (λf'. (λf''. (λx. (λt. (λf'''. t)) (x x)) (λx'. (λt'. (λf'''2. t')) (x' x'))))
  ⋮
  … stopped after 60 steps; the displayed term is partial.

An ever-growing tower λf. λf'. λf''. … — folklore calls such terms ogres: they devour any number of arguments and are never satisfied. And a fixed point of NOT? Classically, \(X = \neg X\) has no solution at all; here reduce Y NOT obligingly builds one, queueing up alternating FALSE/TRUE arguments that the poor Boolean will never finish consuming:

β-reduction (normal order · highlight = next redex)
  start:  (λf. (λx. f (x x)) (λx'. f (x' x'))) (λp. p (λt. (λf'. f')) (λt'. (λf''. t')))
  →β      (λx. (λp. p (λt. (λf. f)) (λt'. (λf'. t'))) (x x)) (λx'. (λp'. p' (λt''. (λf''. f'')) (λt'''. (λf'''. t'''))) (x' x'))
  →β      (λp. p (λt. (λf. f)) (λt'. (λf'. t'))) ((λx. (λp'. p' (λt''. (λf''. f'')) (λt'''. (λf'''. t'''))) (x x)) (λx'. (λp''. p'' (λt'''2. (λf'''2. f'''2)) (λt'''3. (λf'''3. t'''3))) (x' x')))
  ⋮
  … stopped after 60 steps; the displayed term is partial.

What does it mean to “solve” \(X =_\beta \mathrm{NOT}\,X\)? Only this: the equation holds as β-convertibility between terms without normal forms. Y NOT is not TRUE and not FALSE; it is a third thing, a perfectly legal term that no context can ever force to a Boolean answer. This universality of fixed points is simultaneously the calculus’s superpower (general recursion: Fibonacci in the Grand calculations chapter runs on exactly this Y) and its original sin — in Church’s first system, where terms doubled as propositions, a fixed point of negation is the Kleene–Rosser/Curry paradox waiting to happen, and it is precisely why consistent type theories must evict Y and earn recursion some other way. One honest caveat, verified: don’t ask equiv to certify the fixed-point equation —

equiv Y NOT = NOT (Y NOT)

Inconclusive: at least one side did not reach β-normal form within the limit.

equiv works by normalizing both sides, and neither side terminates. The convertibility is real (the reduce Y g trace above is the proof), but it lives one level up from what a normalize-and-compare procedure can see. More on this at the chapter’s end.

The combinator zoo#

In 1924 — before Church, before the λ — Moses Schönfinkel showed that all of logic’s variable-shuffling could be done by a handful of fixed “building blocks”. Haskell Curry rediscovered and systematized them, and his 1930 dissertation made the letters canonical. The zoo’s residents, in the lab’s let syntax (definitions are session-local; defs lists them): start with let S = \x y z. x z (y z) and continue:

let K = \x y. x
let I = \x. x
let B = \f g x. f (g x)
let C = \f x y. f y x
let W = \f x. f x x

(One easter egg on the way in — the lab annotates let K = \x y. x with = TRUE  (Church boolean). K is TRUE, just as FALSE is 0: the pun section above, striking again.)

Now ask ch term for each combinator’s principal type, and something wonderful happens: the zoo turns out to be a textbook of implicational logic. Verified with ch term on each body:

Combinator

Term

Principal type

As a logic law

S

λx y z. x z (y z)

(α → β → γ) → (α → β) → α → γ

Frege’s axiom (distribution)

K

λx y. x

α → β → α

a fortiori (weakening)

I

λx. x

α → α

identity

B

λf g x. f (g x)

(α → β) → (γ → α) → γ → β

hypothetical syllogism (composition)

C

λf x y. f y x

(α → β → γ) → β → α → γ

exchange of premises

W

λf x. f x x

(α → α → β) → α → β

contraction of premises

Every row is a tautology of minimal logic, and ch type will happily reprove any of them from the proposition side — with a Lean-ready witness. For S:

ch type (A -> B -> C) -> (A -> B) -> A -> C

╭──────────────── Found proof ────────────────╮
│ Goal:         (A → B → C) → (A → B) → A → C │
│ Lambda-term:  λp q r. p r (q r)             │
╰─────────────────────────────────────────────╯
╭─────────────────────────────── Lean ───────────────────────────────╮
│ theorem ch_proof {A B C : Prop} : (A → B → C) → (A → B) → A → C := │
│   fun p q r => p r (q r)                                           │
╰────────────────────────────────────────────────────────────────────╯

The search found S. It had to: by Curry–Howard, being the principal inhabitant of that type is what S is. Curry’s deeper observation was structural: B, C, K, W form a complete basis, and each one embodies exactly one bookkeeping right you may exercise over hypotheses — compose them (B), reorder them (C), discard them (K), duplicate them (W). Substructural logics are what you get by revoking these rights one combinator at a time: forbid K and you get relevance logic (no throwing hypotheses away); forbid W and contraction dies (each hypothesis used at most once, the road to linear logic). A century-old zoo, and it turned out to be a map of logic’s design space.

SKI in practice: bracket abstraction#

Schönfinkel’s headline theorem is more brutal still: S and K alone suffice. Every closed λ-term — every one — can be rewritten with no λ, no bound variables, no α-renaming headaches, just applications of two constants. The compilation is called bracket abstraction: to eliminate \(\lambda x\) from a body, recurse with three rules:

\[ [x]\,x = \mathbf{I}, \qquad [x]\,M = \mathbf{K}\,M \;\; (x \notin M), \qquad [x]\,(M\,N) = \mathbf{S}\,([x]M)\,([x]N). \]

And I itself? Apply the rules to \(\lambda x.\,x\) viewed as \([x]\,x\) where we refuse to use the first rule. Since \(x = x\,\) appears alone, split nothing; instead note the slick classical answer: \(\mathbf{I} = \mathbf{S}\,\mathbf{K}\,\mathbf{K}\). Why does that work? \(S\,K\,K\,v\) unfolds to \(K\,v\,(K\,v)\) — “give me \(v\), and also this other thing I will ignore” — which is \(v\). Keep the zoo session open and watch, five steps, no waste:

reduce S K K v

β-reduction (normal order · highlight = next redex)
  start:  (λx. (λy. (λz. x z (y z)))) (λx'. (λy'. x')) (λx''. (λy''. x'')) v
  →β      (λy. (λz. (λx. (λy'. x)) z (y z))) (λx'. (λy''. x')) v
  →β      (λz. (λx. (λy. x)) z ((λx'. (λy'. x')) z)) v
  →β      (λx. (λy. x)) v ((λx'. (λy'. x')) v)
  →β      (λy. v) ((λx. (λy'. x)) v)
  →β      v
  β-normal form reached in 5 step(s).

Officially, then:

equiv S K K = I

β-convertibility by normal forms (η is not used)
  left NF:  λz. z
  right NF: λx. x
  equal β-normal forms up to α

— while alpha S K K = I correctly reports ≢α not alpha-equivalent: as raw syntax they are different terms; equality here is a computation, not a spelling check. One worked example of the S-rule to take home: compiling composition. \([f]([g]([x]\,f(g\,x)))\) grinds down to \(\mathbf{S}\,(\mathbf{K}\,\mathbf{S})\,\mathbf{K}\), and the lab confirms the folklore:

equiv S (K S) K = B

β-convertibility by normal forms (η is not used)
  left NF:  λz y z0. z (y z0)
  right NF: λf g x. f (g x)
  equal β-normal forms up to α

This is not just a party trick. Bracket abstraction is a compiler — from λ-calculus to a language with no binders at all — and its descendants (supercombinators, categorical combinators) sat inside real functional-language implementations in the 1980s. When binders get hard, combinators are the traditional escape hatch.

Exercise: the third K is a decoy

The middle argument of S K K is never actually used. Predict what S K S, S K OMEGA, and in general S K M reduce to — then check yourself in the lab before opening the solution.

Solution

S K M x → K x (M x) → x for any M whose application M x we then discard — so every S K M is an identity. The lab agrees:

nf S K S

β-normal form · 4 step(s)
  λz. z

and equiv S K S = I reports equal β-normal forms up to α. Even the scary one is tamed — nf S K OMEGA answers

β-normal form · 4 step(s)
  λz. z

because nf uses normal order, which discards the OMEGA before ever reducing it (watch reduce S K OMEGA: the step λz. (λy. z) ((λx. x x) (λx'. x' x') z) →β λz. z throws the bomb away unexploded). An applicative-order evaluator would diverge instead — one more reason evaluation order is part of the mathematics, not a detail.

de Bruijn’s revenge#

Nicolaas de Bruijn, building the pioneering AUTOMATH proof checker around 1970, got fed up with bound-variable names and, in a famous 1972 paper, deleted them: replace each bound variable by a number counting how many binders sit between it and its own λ. Names become arithmetic; α-equivalence becomes literal identity of strings. The lab’s debruijn command shows the view that proof-assistant kernels — Lean’s included — actually compare.

Two classics. First, terms that look different but are the same. Shadowing makes λx. λx. x look exotic — which x is bound? Run debruijn \x. \x. x and then debruijn \a. \b. b:

  named:    λx x'. x'
  nameless: λ λ 0

  named:    λa b. b
  nameless: λ λ 0

Same nameless skeleton — the inner binder wins, the shadowed outer x is unreachable, and alpha \x. \x. x = \a. \b. b duly reports ≡α alpha-equivalent. (For the same reason λx y. x (x y) and λf x. f (f x) — which share only one letter — are both λ λ 1 (1 0): the numeral 2 in disguise, twice.)

Second, terms that look nearly identical but differ. The classic exam trap: is λx. λy. x the same as λx. λx. x? One letter apart —

debruijn \x. \y. x

  named:    λx y. x
  nameless: λ λ 1

λ λ 1 versus λ λ 0: the first returns the outer argument (it is K, alias TRUE), the second the inner (FALSE, alias 0). alpha \x. \y. x = \x. \x. x answers ≢α not alpha-equivalent, and no amount of renaming will ever connect a 1 to a 0. That is de Bruijn’s revenge on the naming disputes of mathematical prose: once names are gone, every question about binding has a mechanical, kernel-checkable answer — which is exactly how Lean can compare your proof terms without ever asking what you meant by x.

Numbers are for-loops#

By now the theme is unmistakable, so let us say it plainly: a Church numeral is not a datum that represents \(n\) — it is the control structure for i in 1..n. Everything numerals “are” in this calculus follows from taking that literally.

Iterate a Boolean flip three times from TRUE and you have computed the parity of 3 — run nf 3 NOT TRUE:

β-normal form · 11 step(s)
  λt f. f
  = 0 / FALSE  (the same untyped Church term)

while nf 4 NOT TRUE and nf 10 NOT TRUE both come back = TRUE  (Church boolean) (14 and 32 steps): even numbers of flips cancel. Iterate the successor and you have addition with no PLUS in sight — nf 3 SUCC 4:

β-normal form · 11 step(s)
  λf x. f (f (f (f (f (f (f x))))))
  = 7  (Church numeral)

Three is “do it three times”; do successor three times to 4 and you have 7. (Indeed the official PLUS m n f x = m f (n f x) is just this idea inlined.) Iterate an iterator and you have exponentiation — the tower nf 2 2 2 f x applies f exactly \(2^{2^2}=16\) times:

β-normal form · 44 step(s)
  f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))

And the predecessor legend that opened this chapter was the same move with a compound loop body: n SHIFT (PAIR 0 0) is a for-loop over a two-field state. Church’s encoding anticipated, by several decades, a slogan the functional programmers would later sell as new: data is defined by how you fold over it.

Exercise: predict the parity

Without running it: what is nf 5 NOT FALSE — and roughly how many steps should it take, given that nf 3 NOT TRUE took 11 and nf 4 NOT TRUE took 14?

Solution

Five flips starting from FALSE: odd, so TRUE. The step count grows by 3 per extra flip:

β-normal form · 17 step(s)
  λt f. t
  = TRUE  (Church boolean)

Honest infinity#

For the finale, ask the lab the most innocent question in mathematics — is a thing equal to itself? Run equiv OMEGA = OMEGA:

Inconclusive: at least one side did not reach β-normal form within the limit.

The lab just declined to affirm that Ω equals Ω. Before you file a bug report, note that it is perfectly capable of the syntactic observation — alpha OMEGA = OMEGA instantly answers ≡α alpha-equivalent. What it refuses to certify is β-convertibility, because its equiv is a specific algorithm: normalize both sides, compare up to α. Ω has no normal form, the fuel runs out, and the algorithm reports precisely what it knows: nothing.

This is not a weakness of one little web lab; it is the shape of the theorem. Church proved in 1936 — in the very paper that introduced what we now call Church’s Thesis, months before Turing’s machines — that β-convertibility of λ-terms is undecidable: no algorithm answers correctly on all pairs. What remains is semi-decidability: if two terms are convertible, a patient search will eventually find a common reduct and say yes; if they are not, no general method can be counted on ever to say no. An honest terminating tool therefore has exactly three outputs — yes, no, and I ran out of fuel — and collapsing the third into either of the first two would be a lie. Every “Step limit reached — this is not claimed to be a normal form” you have seen in this chapter is that third answer, worn as a badge.

The sting in the tail: sometimes we can settle what the algorithm cannot. Consider equiv Y I = OMEGA — also Inconclusive, both sides diverge. But you can prove by hand that they are not convertible: the only reduct of Ω is Ω itself, while every reduct of Y I is of the form \(I^k(W W)\) for \(W = \lambda x.\, I\,(x\,x)\) — and by the Church–Rosser theorem, convertible terms must share a common reduct, which these two term families visibly never do. A human argument, using a confluence theorem about the rewriting system, decides a case the general procedure inside it cannot. That is the correct final image for this chapter: the lab is scrupulously honest about the boundary of mechanical knowledge — and mathematics is what you do standing on the far side of it.

Where this connects

  • Lecture 2 — λ-calculus — β, η, normal forms, Church encodings and Y: the theory behind every trick in this chapter.

  • Lecture 1 — type theory — why \x. x x is untypable, and how types buy back termination by evicting the Ω zoo.

  • Lecture 3 — propositional logic — the combinator zoo’s types as axioms; ch type as a proof search you can also drive by hand with prove.

  • Cheatsheet — every command used here (reduce, nf, eta, debruijn, alpha, equiv, let, church, decode, ch) on one page.

Contents