Proving normalization for type theories — that is, that every term in the type theory reduces to a normal form — is difficult. Indeed, in a profound sense, it must be: Gödel’s Second Incompleteness Theorem tells us that theories of the strength we are interested in necessarily require even stronger meta-theories to analyze. And normalization implies consistency, since proofs in normal form may be easily shown not to derive False.
How strong a type theory do we need? The proper answer is: “need for what”? If we are devising a type theory for general mathematics, then in most cases, it does not need to be terribly strong. This is the surprising conclusion of Reverse Mathematics, which seeks to determine what logical principles are truly needed to derive particular mathematical theorems of interest (thus working in reverse, from theorems to the axioms needed to prove them). As Solomon Feferman reports in “In the Light of Logic” (which I am commenting on in other entries on this blog), a little bit of expressive mathematical power goes a long way, and mainstream mathematics rarely truly needs profoundly proof-theoretically complex theories.
What about program verification? Do we need a really strong type theory there? I believe the answer is no. Verifying typical programs should not require proof-theoretically complex reasoning. Indeed, to paraphrase Bill Gates, should be enough for anybody. This is the proof-theoretic ordinal associated with Godel’s System T, which allows definition of simply typed functions by (simply typed) lambda abstraction and primitive recursion: you define the function’s value for , and then express its value for as a function of its value for . The functions definable in System T are exactly the ones which can be proved terminating in Peano Arithmetic, where we have basic axioms for functions like addition and multiplication on natural numbers, and an induction scheme that allows us to conclude if we can show and from , for arbitrary . Indeed the form of this induction scheme is very similar to the form of primitive recursion in simple types. The simple types in primitive recursion correspond to the formulas in the induction scheme.
While neither this form of primitive recursion nor induction may seem terribly complex, looks can be deceiving: it is very easy to prove termination for Ackermann’s function — a fantastically complex function, which is nevertheless just the tip of the iceberg for functions that can be defined in type theories like System T — by this natural form of induction, or to define it by this form of primitive recursion. We’ll look now just at the proof of termination, although the definition in System T is also quite interesting (it can almost be gleaned from the form of the termination proof). We’ll use the following definition of Ackermann’s function, operating on pairs :
The proof of termination can be done straightforwardly by well-founded induction on the pair in the lexicographic ordering (where is greater than iff or else and ). The point I want to highlight here (well-known to proof theorists, but perhaps less so to us computer scientists) is that the simple natural-number induction of Peano Arithmetic is sufficient for this proof, without needing to postulate induction for lexicographic orders. We must simply use a nested induction: an outer induction on , with an inner induction on (the definition of Ackermann’s function in System T uses nested primitive recursion, where the outer recursion is at type ).
So for the outer induction on : in the base case, termination of follows for all by the definition: we simply have . Now assume an arbitrary , and assume that is terminating for all . We must show is terminating, for all . We will do this by inner induction on . If , we have , and termination of the latter expression follows by the outer induction hypothesis. If , then we have . By the inner induction hypothesis, terminates with some value , say (we can apply the inner induction hypothesis since we have ). Now by the outer induction hypothesis, also terminates, and we are done.
Coming back to the question of how strong a type theory we need: unless our goal is proving consistency of strong type theories, we do not need a very powerful type theory. System T, which is considered quite tame by proof-theoretic standards, is already strong enough to analyze wildly infeasible functions like Ackermann’s function (and well beyond, into the so-called Wainer hierarchy). Indeed, we might wonder if we could do with a weaker theory, since after all, the consistency proof of System T (necessarily!) requires more complex reasoning than finitely nested inductions — we might want something a little simpler. There is one practical reason not to go too much weaker: while most practical programs might not truly need such powerful reasoning as embodied in System T/Peano Arithmetic, such reasoning can be much more convenient. A function might be
terminating because some qualitatively complicated natural-number measure of its arguments is decreasing. It might require less thought and work, though, to analyze the function using an unnecessarily powerful lexicographic ordering: subtle observations needed for a single natural-number measure (weighting different factors differently, using exponentials for some) can be completely subsumed by the power of a simple lexicographic ordering.
So in the end, my vote is that System T provides the right level of power for practical program verification. Nevertheless, System T’s meta-theory still requires either a fairly involved ordinal-based argument or the intricate Tait reducibility method (where we obtain a suitably strong induction hypothesis by giving a primitive recursive definition for the formula itself which we are trying to prove). In a subsequent post, I hope to tell you about my frustrations trying to apply a qualitatively simpler approach to consistency based on
so-called hereditary substitutions to System T.