One type up

What a proof about numbers can compute listed every detour-free proof of $N \to N$ up to size 16, where $N$ is the formula $(o \to o) \to o \to o$ whose proofs are the numerals, and ran each one. The 299 functions they compute are all extended polynomials — a free value at zero, then a polynomial with non-negative coefficients — and the predecessor $n \mapsto n - 1$ is not among them, for a reason one line long: such a polynomial that vanishes at 1 vanishes everywhere after.

That essay ended by pointing out where the obstacle lies. A numeral is an iterator: $\lambda f.\ \lambda x.\ f\,(f\,(f\,x))$ applies whatever it is given three times. In the formula $N \to N$, the input numeral is a proof of $(o \to o) \to o \to o$, so the only things it can iterate are functions from $o$ to $o$ — in effect, the successor and things built from it. But the same numeral, as a term, would iterate anything. The term $\lambda f.\ \lambda x.\ f\,(f\,(f\,x))$ proves $(\sigma \to \sigma) \to \sigma \to \sigma$ for every formula $\sigma$; write that formula $N[\sigma]$. A proof of $N[\sigma] \to N[o]$ takes a numeral that is allowed to iterate at type $\sigma$ and returns an ordinary one. This essay asks what changes as $\sigma$ grows, by running the same exhaustive enumeration at four choices of $\sigma$.

The first panel is the previous essay’s result: every line grey. In the second, warm lines leave the panel almost at once — exponentials. In the third, warm lines fall as well as rise; something is computing functions that decrease. In the fourth, with the input iterating a pair of values, the warm lines zigzag. Each change of type has opened a different door.

The same enumeration, at four types #

The method is unchanged from the previous essay. A detour-free term in long normal form is a finite tree whose size counts each $\lambda$ and each variable occurrence, and the terms of each type and size can be listed completely by recursion on the type. Each term is applied to the numerals 0 to 9, which as programs iterate at whatever type they are asked to, and its output is read off. Some terms now grow so fast that their outputs cannot be counted out — a term that computes a tower of exponentials gives an astronomically large numeral at $n = 9$ — and those are recorded as too large rather than evaluated.

The counts run against intuition. Raising the input’s type makes terms rarer: at size 16 there are 9,133 terms with the input at type $o$, 1,953 at $o \to o$, 1,705 at $(o \to o) \to o$ and 505 at $o \to o \to o$. A numeral at a higher type is harder to use, because every place it can be used needs a step function of a more complicated type, and building one costs nodes. Yet the rarer terms reach further. The richer types compute fewer functions in total within the size limit, and more kinds of function.

Exponentials, one type up #

With the input at $o \to o$, the step function the numeral iterates takes a function from $o$ to $o$ and returns another. The obvious such step is composition with itself: given $g$, return $g \circ g$. Iterating that $n$ times starting from the successor gives the successor composed with itself $2^n$ times.

The enumeration finds $2^n$ at size 13, $2^n - 1$ at the same size, and $3^n$ at size 14, followed by a crowd of exponentials with different bases and offsets: on a logarithmic scale they are straight lines of different slopes. The base is the number of times the step composes its argument with itself: $g \mapsto g \circ g$ gives powers of 2, $g \mapsto g \circ g \circ g$ powers of 3, and the offsets come from where the iteration starts and what is applied at the end. None of them is reachable with the input at type $o$, since an exponential is not a polynomial. Raising the type has added exactly one more level of growth. At the next type up, terms that iterate “double the number of doublings” give towers $2^{2^{n}}$, and twelve of the terms at type $(o \to o) \to o$ up to size 17 produce outputs so large at $n = 9$ that two million steps of counting do not reach them.

Each step up in type adds at most one level to such a tower, and this is a general fact rather than a feature of the sizes searched: every function computed by a term of the simply typed λ-calculus, with the input at any fixed type, is bounded by a tower of exponentials whose height depends on the type, and so every one of them is elementary in the sense of computability theory. An ordinal as a growth rate measured how far beyond the elementary functions a system with real recursion reaches. Raising types climbs the elementary hierarchy, and only that.

The towers have been met before. A lemma, and the proof that never mentions one found that removing the lemmas from a proof can multiply its length by a tower of exponentials, and that the height of the tower grows with the complexity of the lemmas’ formulas. Here the same tower is visible from the other side. A term with the input at a higher type is a proof with a lemma of higher type in it — the step function — and normalising it, which is running the program, takes as long as the tower is tall. The growth rate of what a term computes and the cost of removing its detours are one quantity measured twice.

The predecessor, two types up #

The exponentials could have been guessed. The predecessor is the real test, because it has to do something the extended polynomials could not: produce a smaller output from a larger input.

With the input at $(o \to o) \to o$, the enumeration finds the predecessor at size 15, and nothing at the two lower types computes it at any size searched — nor can it, at type $o$, by the previous essay’s argument. The term is short enough to read. Its input iterates a step $\lambda y.\ \lambda z.\ z\,(y\,f)$ — something that takes the state so far, $y$, and returns a new state, which is itself waiting for a function $z$. It starts from the state $\lambda y.\ x$, which ignores whatever it is given and returns zero. And when the iteration is done, it gives the final state the identity function, “do nothing”.

The state after $k$ steps is $\lambda z.\ z\,(f^{k-1}\,x)$: it holds $k - 1$ applications of $f$ and is waiting to be told what to do with one more. Given the successor, it applies it and answers $k$. Given the identity, it does not, and answers $k - 1$. Every step of the iteration feeds the previous state the real successor — so the count inside keeps pace — while the final state is fed nothing, so one application is lost at the end. The state carries two numbers at once, the count and the count less one, and which one comes out depends on what it is given.

That is the trick Stephen Kleene found in 1932, when the predecessor was the standing obstacle to computing with Church’s numerals: iterate on pairs $(k - 1, k)$, starting from $(0, 0)$ and stepping $(a, b) \mapsto (b, b + 1)$, and read off the first component at the end. The term the enumeration found is the same idea with the pair folded into a single function of higher type. A pair of numbers is something that, given a choice of component, returns one of them; a function of type $(o \to o) \to o$ that returns $k$ or $k - 1$ according to the function it is handed is a pair in exactly that sense. The search was told nothing about pairs. It found one because a pair was the shortest way to compute the function.

A pair of values, three functions at once #

Pairs can also be made more directly. A term of type $o \to o \to o$ takes two values and returns one of them, or some combination; iterating at that type means each step of the numeral handles two values at once.

At that type the predecessor appears at size 16, and so do two functions nothing at the other three types reached: parity, $n \bmod 2$, and halving, $\lfloor n/2 \rfloor$. Parity is the clearest. A term of type $o \to o \to o$ can be a Church boolean, $\lambda t.\ \lambda u.\ t$ for true and $\lambda t.\ \lambda u.\ u$ for false; iterating the step “swap the two arguments” $n$ times starting from true gives true or false according to whether $n$ is even, and applying the result to 0 and 1 reads it off. Halving keeps a pair of counts and moves one unit between them on alternate steps. None of the three is an extended polynomial, and parity and halving are reached at none of the other three types within the sizes searched. Each of the four types has its own characteristic functions, the ones it reaches first and most cheaply.

The table also records a loss. The square $n^2$, found at size 11 with the input at type $o$, appears at none of the higher types within the sizes searched. The squaring is still possible there — use the numeral to iterate, at type $o \to o$, the step “compose with the $n$-fold successor” — but the long normal form of that term at a higher type needs more nodes than the search reached. Raising the type does not simply add functions on top of the old ones at the same price; it changes what is cheap.

Running every term is a fair test here #

The whole method of this essay and the last — list every term of a type, run each one, and collect the functions — depends on a property that most programming languages lack. No algorithm can read what a program does proved that for programs in general nothing about their behaviour can be decided, because running one may never finish and there is no way to tell in advance. Every term here finishes. Removing detours from a simply typed term always terminates, so each of the terms listed computes a total function, and running it on ten inputs gives ten answers in a finite time — or, for the towers, in a time so long that the run was stopped and the term recorded as too large to evaluate rather than guessed at.

Two things are still taken on trust and are worth saying. Functions were identified by their values at 0 to 9; two terms that agree there and differ at 10 would be counted as one function. For the extended polynomials of low degree that cannot happen, and for the exponentials and the functions of pairs found here the patterns are regular enough to make it implausible, but it is a finite check of an infinite statement. And the dashes in the table mean “not found within the sizes searched”, which for $n^2$ at the higher types is demonstrably a matter of size rather than of possibility.

Why the type is the whole story #

The four panels of the hero figure are four answers to one question, and the question is how much structure a single iteration can carry from one step to the next. At type $o$ it carries a number, and the only thing to do with a number is add to it. At $o \to o$ it carries a function, which can be composed with itself, and composition is how exponentials arise. At $(o \to o) \to o$ and at $o \to o \to o$ it carries something that can hold two numbers, and two numbers are enough to remember the previous step. Every function in the figures is a single iteration of the input numeral, possibly nested; the type decides what is passed along.

This is the computational side of something every derivation is a term set out in logical terms. The type of a term is the formula it proves, so raising the input’s type is proving a different formula — not $N \to N$ but $N[\sigma] \to N$. The extended polynomials are what can be proved about numbers when the hypothesis is the plainest formula numbers satisfy. A stronger hypothesis about the input, that it can iterate at a richer type, buys more conclusions.

Still open: one type for all #

The obvious next move is to let a numeral iterate at every type at once. Jean-Yves Girard’s system F, from 1972, does exactly that: it adds quantification over types, and a numeral becomes a proof of $\forall\alpha.\ (\alpha \to \alpha) \to \alpha \to \alpha$, usable at any type inside one term. Using it at a particular type is instantiating that quantifier, the same move as the instance that has to be guessed in a first-order proof, one level up: there a universal claim about individuals is applied to a chosen term, here a universal claim about types is applied to a chosen type, and the choice is exactly what each panel of the hero figure fixed by hand. Subtraction of two inputs, which iterates the predecessor as many times as the second input says, needs the predecessor to take and return numerals at the same type — exactly what the terms here cannot do, since the predecessor found takes its input at a higher type and returns at type $o$, so its output cannot be fed back in. In system F that obstacle disappears, along with every other on this page: Girard proved that the functions it computes are exactly those that second-order arithmetic can prove to be total, a class far beyond anything Gödel’s system T reaches. The price is the proof that it terminates. Girard’s normalisation proof for system F cannot be carried out in second-order arithmetic, since it would show that system consistent, and the sentence that says it has no proof explained why no sufficiently strong system proves its own consistency. The more a typed language can compute, the stronger the logic needed to know that its programs halt.

Between the simply typed terms of this essay and system F lies a large and only partly mapped territory. Which functions become definable when inputs and outputs may be at different fixed types, how the smallest terms for a given function grow with the types allowed, and how much of system F’s power is already present when quantification is restricted to a few levels are questions with partial answers. The enumeration here can ask any of them for small sizes, and the answers it gives — 2ⁿ at size 13, the predecessor at 15 and 16, parity and halving at 16 — are the beginning of such a map, not the map.

What the iteration carries #

The numeral did not change from one panel to the next. The same $\lambda f.\ \lambda x.\ f\,(f\,(f\,x))$ was given four different jobs, and each job was a type. At the lowest it could only add, and every function it computed was a polynomial; one type up, it could compose and so exponentiate; two types up, or iterating a pair, it could carry the previous step along, and the predecessor, parity and halving appeared. An exhaustive search over small terms found each of these at the smallest size it can have, and in the predecessor it rediscovered Kleene’s pair, folded into a function, without being told what a pair was.