Theorem 5.6 (Scott 1981, PRG-19, §5) — recursive functions are λ-definable #
Scott's Theorem 5.6: every partial recursive h : N → N is denoted by a λ-term
whose only constants
are cond, succ, pred, zero, 0. The proof is by the standard generation
of the partial
recursive functions: strict starting functions, closure under (multivariate)
composition,
primitive recursion, and the μ-scheme (least-number operator). We formalise
the constructive
heart of the proof — the actual combinators Scott writes down — over the
natural-number domain N
(Example 4.3) and the conditional cond (Exercise 3.26), proving the defining
equations of each
scheme. (We do not also wire these together against an external inductive
predicate of partial
recursive functions; that closure is a routine but lengthy induction over the
generation grammar,
built entirely from the pieces below.)
What is proved #
Strict starting functions (Scott's "simple device"
λx. cond(zero(x), x, x)):strictIdwithstrictId_natElem(= n̂) andstrictId_bot(= ⊥);strictProj₀ : N × N → N, the strict first projection, withstrictProj₀_natElem,strictProj₀_bot_left,strictProj₀_bot_right(strict in both arguments).
Primitive recursion
primRec f g, the least fixed point!k λx,y. cond(zero(x), f(y), g(pred(x), y, k(pred(x), y))), with the scheme equationsprimRec_zero:hbar(0̂, m̂) = f(m̂),primRec_succ:hbar((n+1)^, m̂) = g(n̂, m̂, hbar(n̂, m̂)),primRec_bot:hbar(⊥, m̂) = ⊥(strict in the recursion argument).
The μ-scheme
muRec f/muMap f, the least fixed point!g λx,y. cond(zero(f(x,y)), x, g(succ(x), y))andhbar = λy. gbar(0̂, y), withmuRec_found:f(n̂, m̂) = 0̂ ⟹ gbar(n̂, m̂) = n̂,muRec_step:f(n̂, m̂) = (j+1)^ ⟹ gbar(n̂, m̂) = gbar((n+1)^, m̂),muRec_bot:f(n̂, m̂) = ⊥ ⟹ gbar(n̂, m̂) = ⊥, and the capstonemuMap_eq_least: ifn₀is the least zero off(·, m̂)(all earlier values positive totals), thenμ(m̂) = n̂₀.
All cond-based maps inherit Classical.choice structurally from the truth
domain T
(Example 1.2) exactly as cond/zeroMap already do; the fixed points come from
Theorem 4.1.
The truth-domain bottom of T agrees with Example23.botElt (both are the
least element).
Needed because zeroMap_bot lands in T.bot while cond_bot is phrased with
Example23.botElt,
and bot is not reducible.
Strict starting functions (λx. cond(zero x, x, x)). #
Scott's strict identity λx. cond(zero(x), x, x): the identity on totals,
⊥ on ⊥.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scott's strict first projection λx₀, x₁. cond(zero(x₁), x₀, x₀) on N × N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
proj₀(n̂, m̂) = n̂.
Strict in the second argument: proj₀(n̂, ⊥) = ⊥.
Strict in the first argument: proj₀(⊥, m̂) = ⊥ (the output is x₀ = ⊥).
Primitive recursion. #
Given f : N → N and g : N × N × N → N (with N³ modelled as N × (N × N)),
the primitive
recursion hbar with hbar(0, m) = f(m), hbar(n+1, m) = g(n, m, hbar(n, m)) is the
least fixed point of
λk λx,y. cond(zero(x), f(y), g(pred(x), y, k(pred(x), y))).
Selector maps on (N×N → N) × (N×N). #
The recursion bodies live over prod F Q with F = funSpace (N×N) N (the
unknown) and Q = N × N
(the argument pair). We name the four selectors once to keep the body terms
readable.
The argument pair ⟨x, y⟩ (= proj₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unknown function k (= proj₀).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two-argument body M(k, ⟨x, y⟩) = cond(zero(x), f(y), g(pred x, y, k(pred x, y))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The primitive-recursion operator R(k) = λx,y. cond(zero x, f y, g(pred x, y, k(pred x, y))).
Equations
Instances For
primRec f g : N × N → N, the least fixed point of primOp.
Equations
Instances For
The defining recursion of primRec.
Primitive recursion, base case. hbar(0̂, m̂) = f(m̂).
Primitive recursion, step case. hbar((n+1)^, m̂) = g(n̂, m̂, hbar(n̂, m̂)).
Primitive recursion is strict in the recursion argument. hbar(⊥, m̂) = ⊥.
The μ-scheme (least-number operator). #
Given f : N × N → N, the minimization hbar(m) = μn. f(n, m) = 0 is obtained from
gbar = !g λx,y. cond(zero(f(x,y)), x, g(succ(x), y)) by hbar = λy. gbar(0̂, y).
The body M(g, ⟨x, y⟩) = cond(zero(f(x, y)), x, g(succ x, y)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The μ-operator R(g) = λx,y. cond(zero(f(x, y)), x, g(succ x, y)).
Equations
Instances For
muRec f : N × N → N, the binary search gbar, least fixed point of muOp.
Equations
Instances For
The minimization μ : N → N, hbar(m) = gbar(0̂, m) (the strict 0-seeded
search).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining recursion of muRec.
μ, found. If f(n̂, m̂) = 0̂, the search stops and returns n̂.
μ, step. If f(n̂, m̂) is a positive total (j+1)^, the search advances
to n+1.
μ is strict in the test. If f(n̂, m̂) = ⊥, the search diverges.
μ(m̂) = gbar(0̂, m̂).
The search advances over a run of positive totals: if f((n+i)^, m̂) is a
positive total for
all i < k, then gbar(n̂, m̂) = gbar((n+k)^, m̂).
Capstone (μ-scheme correctness). If n₀ is the least zero of f(·, m̂)
— that is,
f(n̂₀, m̂) = 0̂ and f(î, m̂) is a positive total for every i < n₀ — then
μ(m̂) = n̂₀.