Nottingham FP Lab Blog

Archimedes, Gentzen and lenses

by Hancock on October 20, 2007.
Tagged as: Lunches.

At Neil’s request, I talked on the topic of “lenses”, a name I use for a structure underlying many well-ordering proofs. (The same name is used by some people for funny-bracket notation for anamorphisms, catamorphisms, and the like. The notions have nothing to do with each other, except insofar as initial algebras are involved.)

I started by explaining “Archimedes trick”, involved in his work the “Sand Reckoner”. See http://en.wikipedia.org/wiki/The_Sand_Reckoner.

Call a predicate an accessibility predicate if it holds of 0, and is closed under the successor operation. If A is an accessibility predicate, we can evidently find a proof that it holds of 2^17, using some 130,000 applications of Modus Ponens. The problem is to give a short proof (without using induction).

The trick is to define the following predicate:

A_1(y) = all x. A(x) -> A(x + 2^y).

Observe that this too is an accessibility predicate. So we can give quite a short proof of A_1(17), using about 17 applications of Modus Ponens. But then, we’re done, as A_1(17) implies A(2^17).

How about 2^2^17? Same deal. Define

A_2(y) = all x. A_1(x) -> A_1(x + 2^y).

Obviously this too is an accessibility predicate, so we get a short proof that A_1(2^17), and then, in a trice, a short proof of A(2^2^17). Essentially, we just play the same trick again.

I then pointed out that the same trick works in the case of the second number class, meaning the initial algebra for the functor

X |-> 1 + X + X^N,

data Omega = Zero | Succ Omega | Lim (Nat -> Omega).

For example, we have the usual finite ordinals 0, S(0), S(S(0)), .. and the first infinite ordinal $\omega$ = L(\n. S^n (0)).

We also have addition, multiplication and exponentiation, defined (by recursion, ie. initiality):

a + 0 = a
a + S(b) = S(a + b)
a + L(f) = L(\n. a + f(n))

a * 0 = a
a * S(b) = (a * b) + a
a * L(f) = L(\n. a * f(n))

a ^ 0 = S(0)
a ^ S(b) = (a ^ b) * a
a ^ L(f) = L(\n. a ^ f(n))

(Note: all three are continuous in their second argument — meaning they “commute with limits”.)

Call a predicate an accessibility predicate if it holds of 0, is closed under the successor operation, and is also closed under limits, in the sense

all f : Nat -> Omega. (all n : Nat. A(f(n))) -> A(Lim(f))

Consider the problem of proving A( $\omega$ ^ $\omega$ ), but without induction on Omega. We just use Archimedes’ trick, more usually called Gentzen’s trick in this context.

Define A_1(y) = all x. A(x) -> A(x + $\omega$ ^y).

This too is an accessibility predicate. So we can easily show A_1( $\omega$ ). But then we’re done, as this implies A( $\omega$ ^ $\omega$ ).

Again, we can iterate the trick, and prove, A(omega^omega^omega), A(omega^omega^omega^omega), and so on. The limit of this sequence of ordinals is traditionally called $\epsilon_0$ . The proofs can actually be written out quite easily in the usual systems of formal arithmetic. (There are, to be honest, some purely bureaucratic problems to overcome.) What we have done, in fancy terminology, is show that the proof-theoretic ordinal of formal arithmetic is at least $\epsilon_0$ .

You can find a version of the proof in (an early version of) Agda at http://homepages.inf.ed.ac.uk/v1phanc1/epsilon0.agda.

I then gave a quick (and only a little dirty) definition of a “denotable ordinal” of a type-theory, such as the simply-typed lambda calculus with the natural numbers, and primitive recursion of all finite types.

Such a thing is given by a term t with 4 free variables X,z,s,l:

X : Set, z : X, s : X->X, l : (N->X)->X |- t[X,z,s,l] : X

For example:

t_{zero} [X,z,s,l] = z
t_{one} [X,z,s,l] = s z
t_{two} [X,z,s,l] = s (s z)
t_{omega}[X,z,s,l] = l (\n->iterate s n z)

Suppose a and b are denotable ordinals, then (I’m sorry, I can’t get this formatted properly!!)
t_{a+b}[X,z,s,l] = t_{b} [ X,t_{a}[X,z,s,l],s,l] t_{a*b}[X,z,s,l] = t_{b} [ X,z,\x->t_{a}[X,x,s,l],l] t_{a^b}[X,z,s,l] = t_{b} [ X->X, s, \f x ->t_{a}[X,x,f,l], \g x ->l (\n -> g n x) ] z
This is essentially Archimedes’ trick. Note that exponentiation requires use of the function space. Without it, we are confined below $\omega$ ^ $\omega$ .

Having used up an hour, I finished up, muttering darkly that the notion of “lens” is an abstraction that generalises what is going on in the definitions above: a kind of “magnification” of a Church-ordinal, by applying it at a higher type.

(By the way, people who know it will recognise that the three definitions above are, apart from the limits, at the heart of Schwichtenberg’s demonstration that the numerical functions expressible in the simply-typed lambda calculus are the “extended polynomials”.

I could give another talk on these topics, showing how to get beyond $\epsilon_0$ . And then, by using a “universe” type (a type of types), how to get all the way up to the next major landmark ordinal after $\epsilon_0$ , namely one called $\Gamma_0$ . If anyone wants.

One can find a lecture by Thierry Coquand on these and similar matters at http://www.cs.chalmers.se/~coquand/ordinal.ps