Skip navigation

How Strong a Type Theory Do We Need?

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, \epsilon_0 should be enough for anybody. This \epsilon_0 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 0, and then express its value for n+1 as a function of its value for n. 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 \forall n\in\mathbb{N}. \phi(n) if we can show \phi(0) and \phi(n+1) from \phi(n), for arbitrary n\in\mathbb{N}. 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 (m,n):

\begin{array}{lll} \mathit{ack}(0,n) & = & n+1 \\ \mathit{ack}(m+1,0) & = & \mathit{ack}(m,1) \\ \mathit{ack}(m+1,n+1) & = & \mathit{ack}(m,\mathit{ack}(m+1,n)) \end{array}

The proof of termination can be done straightforwardly by well-founded induction on the pair (m,n) in the lexicographic ordering (where (m_1,n_1) is greater than (m_2,n_2) iff m_1 > m_2 or else m_1 = m_2 and n_1 > n_2). 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 m\in\mathbb{N}, with an inner induction on n\in\mathbb{N} (the definition of Ackermann’s function in System T uses nested primitive recursion, where the outer recursion is at type \mathbb{N}\to\mathbb{N}).

So for the outer induction on m: in the base case, termination of \mathit{ack}(0,n) follows for all n\in\mathbb{N} by the definition: we simply have \mathit{ack}(0,n) = n+1. Now assume an arbitrary \mathit{m}\in\mathbb{N}, and assume that \mathit{ack}(m,n) is terminating for all n\in\mathbb{N}. We must show \mathit{ack}(m+1,n) is terminating, for all n \in \mathbb{N}. We will do this by inner induction on n. If n = 0, we have \mathit{ack}(m+1,n) = \mathit{ack}(m,1), and termination of the latter expression follows by the outer induction hypothesis. If n = n'+1, then we have \mathit{ack}(m+1,n) = \mathit{ack}(m,\mathit{ack}(m+1,n')). By the inner induction hypothesis, \mathit{ack}(m+1,n') terminates with some value v, say (we can apply the inner induction hypothesis since we have n' < n'+1 = n). Now by the outer induction hypothesis, \mathit{ack}(m,v) 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.

4 Comments

  1. Like me, ordinal-like structures pop up without all that much provocation.

    Here’s the free monad for the read-a-number operation, in Haskell syntax.

    data ReadsNatsMakes a
    = Make a
    | Read (Nat -> ReadsNatsMakes a)

    The bind operation goes like this

    Make a >>= g = g a
    Read f >>= g = Read (\n -> f n >>= g)

    All such processes are guaranteed to stop Read finitely many times before a Make, but there are processes for which there is no uniform finite bound on the number of Read steps which can happen, e.g., reading a number n, then reading n numbers.

    I suspect that proving the monad laws (where return is Make) may be tricky with only natural number induction.

    I don’t know whether this sort of basic I/O programming counts as “practical”. But I think it’s fun.

  2. Hi, Conor.

    This is a cool example. If we tried to index this type by a natural number representing the depth, we’d get in trouble at the Read case (right?). We could get around this by doing something like:

    Read : (f:nat->nat) -> (x:nat -> ReadsNatsMakes a (f x)) -> ReadsNatsMakes a (lub f)

    This definition just says that we must describe the relationship between the input argument x given to the function F given to Read, and the depth of (F x); and if we can summarize that relationship by a function f, then the depth of the Read-term is the least upper bound of the range of f.

    To me it is completely reasonable to consider using ordinals of the second number-class (i.e., countably infinite ordinals) for Trellys. We could take, say, ordinals up to epsilon_0, and include a terminating recursor for those.

    Some monadic examples might be better treated coinductively (not that we have current plans in Trellys for that). There, we could try indexing coinductive types by a coinductive nat. But this is pretty speculative.

    Aaron

  3. Indexing depth by natural numbers won’t cut it, I’m afraid. That rules out those processes with no depth bound, e.g., read number n then read n numbers. There ain’t no lub.

    Inductive definitions are really very powerful, and we use that power, especially when we build universes and write metaprograms, or implement typed DSLs. Programmers writing interpreters may not appreciate low-power induction. It’s worth taking some trouble to supply good tools here.

  4. Conor,

    Sorry my comment was not clear: I agree with you that we might want to index by an ordinal. I meant to write:

    Read : (f:nat->ord) -> (x:nat -> ReadsNatsMakes a (f x)) -> ReadsNatsMakes a (lub f)

    So the lub is a lub on a set of ordinals, not a set of naturals (and so it does exist).

    About writing interpreters: my attitude is that most programmers will be satisfied with general-recursive interpreters. That is, they won’t really care whether or not the type system can certify the interpreter is really terminating. If you want a System F interpreter that is statically certified to be terminating — well, one should expect to do some work there (which would be possible in Trellys, if we take our proof language to be strong enough).

    Have fun at DTP! I’m sorry I can’t be there, but I absolutely have to be at FLoC for the second half, and 2 weeks is too long to be away from home. Say hi to Vilhelm (Sjoeberg) if you see him.

    Aaron


Leave a comment