What a proof about numbers can compute

Every derivation is a term turned proofs into programs. A natural-deduction derivation is a term of the typed λ-calculus, the formula it proves is the term’s type, and a detour — a lemma proved and at once used — is a term that can be simplified, so removing detours is running the program. Along the way it noticed something about one small formula. The proofs of $(p \to p) \to (p \to p)$ without detours are $\lambda f.\ \lambda x.\ x$, $\lambda f.\ \lambda x.\ f\,x$, $\lambda f.\ \lambda x.\ f\,(f\,x)$, and so on: one for each number of times the assumed implication $f$ is used. The proofs of that formula are the whole numbers.

This essay takes the next step, which Alonzo Church took in the 1930s and Helmut Schwichtenberg completed in 1976. Write $N$ for the formula $(o \to o) \to o \to o$, with $o$ a single atom. A proof of $N \to N$ assumes a number and produces a number. Apply it to the proof that is the numeral 3, remove the detours, and what is left is a numeral: the proof has computed a function. The question is which functions proofs of this one formula can compute, and the answer is precise, surprisingly small, and found here by listing every such proof up to a size and running each one.

A numeral is an iterator #

The numeral $n$ is the proof $\lambda f.\ \lambda x.\ f\,(f\,(\cdots(f\,x)\cdots))$ with $n$ copies of $f$. Read as a program it takes a function and a starting value and applies the function $n$ times. That is the only thing a numeral can do, and every proof of $N \to N$ has to work through it.

The four proofs in the figure show the possibilities. The first, $\lambda n\,f\,x.\ n\,(\lambda y.\ f\,y)\,(f\,x)$, starts from $f\,x$ — one application already made — and lets the input apply $f$ a further $n$ times: $n + 1$. The second lets the input iterate “apply $f$ twice”: $2n$. The third iterates “apply $f$ as many times as the input says”, nesting the input inside itself: $n \cdot n$. The fourth iterates a constant function, $\lambda y.\ x$, starting from $f\,x$: if the input is 0 nothing is iterated and the answer is $f\,x$, which is 1; if it is anything else, the first iteration throws the $f\,x$ away and the answer is $x$, which is 0. That is a test for zero, and it is the only way a proof of this formula can look at its input without simply using it as a count.

The terms are written in the form the earlier essays called detour-free, and in the slightly stricter form called long normal: every variable is applied to all the arguments its type allows, so the successor appears as $\lambda y.\ f\,y$ rather than bare $f$. In that form a proof of $N \to N$ is a finite tree, its size is the number of nodes — each $\lambda$ and each variable counts one — and the proofs of a given size can be listed completely. A variable’s type says how many arguments it takes and of what types, so building a proof of type $o$ means choosing a variable whose type ends in $o$ and building proofs for each of its arguments; that recursion is the whole of the enumeration.

Running a proof #

It is worth watching one of these proofs compute, because the computation is nothing but the removal of detours that the earlier essays defined. Take the doubling proof $D = \lambda n.\ \lambda f.\ \lambda x.\ n\,(\lambda y.\ f\,(f\,y))\,x$ and the numeral $3 = \lambda g.\ \lambda z.\ g\,(g\,(g\,z))$. The application $D\,3$ is a detour: $D$ proves an implication by introducing it, and the application at once uses it. Removing it substitutes the numeral for $n$:

$$\lambda f.\ \lambda x.\ 3\,(\lambda y.\ f\,(f\,y))\,x.$$

Inside, $3$ is again an introduction immediately used, and substituting gives $(\lambda y.\ f\,(f\,y))$ applied three times to $x$. Each of those applications is a detour of its own, and removing them one by one leaves

$$\lambda f.\ \lambda x.\ f\,(f\,(f\,(f\,(f\,(f\,x))))),$$

the numeral 6. Nothing was evaluated in any sense beyond substitution; the arithmetic is the bookkeeping of the assumption a proof pays back, carried out until no assumption is introduced and immediately discharged. The enumeration reads off the same answer faster, by interpreting $f$ as adding one and $x$ as zero, but the two readings agree by construction, and the first is the one that makes the output a proof.

Fourteen thousand proofs, three hundred functions #

Running the enumeration to size 16 lists 14,659 proofs of $N \to N$.

Each proof was applied to the numerals 0 to 9 and its ten outputs recorded, by reading $o$ as the natural numbers, $f$ as adding one and $x$ as zero — which is exactly what removing the detours and counting the copies of $f$ in the resulting numeral would give. Two proofs compute the same function if their ten outputs agree. The proofs multiply about two and a half times with each step in size; the functions accumulate far more slowly, 299 in all, because most proofs are different routes to an output that some smaller proof already reaches. The constant 2, for instance, is computed by one proof of size 6, $\lambda n\,f\,x.\ f\,(f\,x)$, which ignores its input, and by dozens of larger proofs that consult the input and then throw away what it said.

The first thing to notice about the 299 is what they have in common.

Every function on the list has the same shape. At $n = 0$ it takes some value; from $n = 1$ on it is a polynomial in $n$ whose coefficients are whole numbers, none of them negative. Some are plain polynomials — $n + 2$, $2n + 1$, $n^2$ — whose value at 0 is the polynomial’s own. Others do one thing at zero and another everywhere else: 3 at zero and 1 after, or 0 at zero and 4 after. Schwichtenberg called these the extended polynomials, and his theorem of 1976 is that they are exactly the functions computed by proofs of $N \to N$. Every extended polynomial has a proof, and every proof computes one. The table is that theorem checked from the computational side, on all 299 functions the enumeration found: each set of ten values was fitted exactly by a polynomial from $n = 1$ on, and the coefficients came out whole and non-negative every time.

Polynomials by nesting #

Why polynomials? Because the only operations available are the ones a numeral performs. Iterating a function $n$ times and composing iterations gives sums and products of counts, and nothing else.

The power $n^k$ needs the input nested $k$ deep: $n$ applied to “apply $n$ applied to ‘apply $n$ … to $f$’”. Each level of nesting costs three nodes — a use of the input and a fresh $\lambda$ for the value it iterates — so $n$ appears at size 8, $n^2$ at 11 and $n^3$ at 14, and the enumeration stops before $n^4$, which would need size 17. Sums come from starting one iteration where another finished; products come from iterating an iteration. A constant offset at zero comes from the test in the hero figure: iterate a function that discards its argument, and whether anything was iterated at all becomes visible in the result.

What is missing is any way to go down. The input can be used as often as wanted, at any depth, but each use is an instruction to repeat something some number of times. There is no instruction to repeat something one fewer time than the input says, and no way to undo an application of $f$ once it has been made.

The other half of the theorem, that every extended polynomial has a proof, is a matter of assembling pieces the figures already show. A constant $c$ is $c$ applications of $f$ that ignore the input. The input itself is $n$ iterating $f$. Given proofs of two functions, their sum starts the second where the first leaves off — iterate $f$ the second number of times, starting from the first’s output — and their product iterates the first’s “apply $f$ that many times” as often as the second says. That builds every polynomial with non-negative whole coefficients. The free value at zero comes from the test. Iterate, $n$ times, a function that ignores its argument and returns the polynomial’s value $p(n)$, starting from the value wanted at zero: if $n$ is 0 nothing is iterated and the starting value survives, and if $n$ is anything else the first iteration replaces it by $p(n)$ and the later ones change nothing. Every extended polynomial is a combination of these, so each has a proof, and the enumeration finds each one at the size its construction predicts or smaller.

The empty place #

That absence can be seen directly.

The predecessor function — $n - 1$, with $0 - 1$ taken to be 0 — has value 0 at 1 and value 1 at 2. Among the 299 functions, ten have value 0 at 1, and every one of them is 0 at 2, and at 3, and at every $n$ from 1 on. The reason is one line. From $n = 1$ on an extended polynomial is a polynomial $a_0 + a_1 n + a_2 n^2 + \cdots$ with every $a_i \ge 0$; its value at 1 is $a_0 + a_1 + a_2 + \cdots$, a sum of non-negative numbers, and that sum is 0 only if every coefficient is 0. So an extended polynomial that vanishes at 1 vanishes everywhere after it, and the predecessor, which vanishes at 1 and nowhere else, is not one. The same argument removes any function that is zero at some $n \ge 1$ without being zero from then on — in particular every form of subtraction.

The figure shows something else as well: the whole region below the diagonal is empty. No function is smaller at 2 than at 1, because a polynomial with non-negative coefficients never decreases. Proofs of $N \to N$ compute functions that can stand still or climb, and that is all.

Church’s original encoding met this obstacle in 1932, and the predecessor was then thought by some to be beyond the λ-calculus altogether. Stephen Kleene found a way round it, famously while at the dentist, but the way round uses something the typed setting of this essay does not allow at the type $N \to N$: it iterates on pairs, which requires the input numeral to iterate at a more complicated type than $o$. One type up is about exactly that.

Two inputs #

The same enumeration can be run on proofs of $N \to N \to N$, which take two numerals and return one.

All 10,267 proofs of $N \to N \to N$ up to size 15 compute 877 different functions of two numbers. Addition appears at size 13 — iterate the successor $m$ times starting from where $n$ iterations left off — and multiplication, surprisingly, one size earlier, since iterating “apply $f$ $n$ times” $m$ times is a shorter term than chaining two iterations end to end. Size here measures how much proof a function needs, which is not the same as how hard the function looks. Tests on zero appear, as in one variable: “$m$ if $n$ is 0, and 0 otherwise”.

Five familiar functions are not there, and Schwichtenberg’s theorem says they never will be. The larger of $m$ and $n$, the smaller of them, $m - n$ stopped at zero, and the test for whether $m = n$ all need some comparison of the two inputs, and an extended polynomial in two variables cannot compare: it can test each input for zero separately and otherwise only add and multiply. And $m^n$ is not a polynomial at all; computing it needs one numeral to iterate the other numeral, which means using $m$ at the type of an iterator rather than at type $o$, and the formula $N \to N \to N$ does not permit that. Exponentiation, like the predecessor, is waiting one type up.

A small class, and why it is small #

The class is small for a reason that has recurred since the lemma and the proof that never mentions one. Every proof here terminates: removing detours from a typed term always finishes, so every proof of $N \to N$ computes a total function, defined at every input. That is a strength — no proof can loop — and it has a price. No algorithm can read what a program does showed that any language in which every program halts must leave out some computable total functions, since otherwise its halting problem would be trivial and the diagonal argument would go through. A language of proofs that always normalise cannot compute everything.

What is unusual about this case is how much it leaves out. Gödel’s system T, which adds a recursion operator to the typed λ-calculus, computes every function that Peano arithmetic can prove total, a class that an ordinal as a growth rate measured by the ordinal $\varepsilon_0$. The pure typed λ-calculus with numerals at a single type computes the extended polynomials — not even the predecessor. The gap between those two classes is the whole difference between a system that has a principle of iteration built in and one that has only the iteration a numeral happens to carry. It is also a gap in proving power. Gödel used system T to give a consistency proof of arithmetic, by interpreting each theorem as a program and showing that the programs halt; the sentence that says it has no proof explained why such a proof must use principles arithmetic itself cannot prove, and system T’s recursion at higher types is where those principles live. Strip the recursion out, as the formula $N \to N$ does, and the halting of every program is easy to prove and what the programs compute shrinks to polynomials. Conway’s fourteen fractions compute everything a computer can and halt on no guaranteed schedule; the proofs here halt always and compute almost nothing.

Still open: when two programs are the same function #

The figures identified two proofs as computing the same function when they agreed on the inputs 0 to 9. For extended polynomials that is a safe test — two of them that agree at ten points from 0 to 9 and have degree at most 8 agree everywhere — and the degrees reached here are at most 3. For general typed terms the question is harder. Two terms of the same type are extensionally equal if they give equal results on every input, and for terms of the simply typed λ-calculus with a single base type, whether two terms are equal in every model was shown by Richard Statman to be decidable, but the problem is non-elementary in the worst case: deciding it can take time exceeding any fixed tower of exponentials in the size of the terms. Whether two proofs of the same formula are the same proof — Hilbert’s twenty-fourth problem, which every derivation is a term left open — is a stricter question still, and for proofs as programs it is the question of when two programs that compute the same function do so in the same way.

Counting, and nothing else #

A proof of $N \to N$ can use the number it is given in exactly one way, as a count of how often to repeat something, and the repetitions can be nested and chained but never reversed. Listing all 14,659 such proofs up to size 16 and running them found 299 functions, every one a polynomial with non-negative coefficients after a free choice at zero, and none that decreases; the predecessor’s place in the plane of values at 1 and 2 is empty, for a reason one line long. The proofs are perfectly good programs and they always finish. What they cannot do is count down.