Complexity of type-checking in relation to complexity of normalization

Question

In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can instead just type-check the program. That will take some time too, sometimes "a lot" too.

I'm looking for results that formalize the relation of the complexity of type-checking to the complexity of normalization for a various type-systems, i.e. possible speedup ratios. Is that relation always well defined? I'm not sure.

But we can give some lower bounds by demonstrating families of typed terms.

I'm interested mostly in any of the well known type systems such as System F, predicative variants of system F, including 'Rank 1' variant and Calculus of constructions. 'Intersection types' are particularly interesting case since they characterize the family of normalizing lambda terms.

Answer 1

The relationship that you're looking for is indeed well-defined, but IMO it's not quite the right thing to look at. For example:

1. Type checking for terms in the simply-typed lambda calculus is linear time, but normalizing terms in the STLC exceeds any fixed tower of exponentials (i.e., $O(2^{2^{2^{\ldots n}}})$.
2. Type checking for System F is linear time, but normalization takes as long as any function definable in second-order arithmetic.
3. For $F^\omega$, typechecking exceeds any tower of exponentials (since you have to normalize simply-typed lambda-terms to do typechecking), but normalization is complete for higher-order arithmetic.
4. Type inference for rank-1 types (basically, ML-style types) is EXPTIME-complete, but normalization time is somewhere in between the STLC and System F.
5. Type inference for intersection types is undecidable (because they characterize halting).

What's going on here is that once you add enough type annotations, typechecking gets easy. If you have to do inference, then the problem gets much harder. This hints that there's a connection between program analysis and evaluation, and the ability of intersection type disciplines to characterize normalization further hints that the key place to look is linear logic.

• A good place to get an intuition is from David Van Horn and Harry Mairson's papers Flow Analysis, Linearity, and PTIME and Relating complexity and precision in control flow analysis.

  These papers show that for a linear calculus, program analysis and evaluation coincide, because linearity makes the approximation of flow analysis exact.

• So by taking a linear calculus and then carefully controlling how much contraction you have via intersection types, you can gain a rather fine control over the complexity of normalization. As you might expect, there is an awful lot of work in this space from the intersection types community.

  So rather than trying to summarize it all and missing important references, I'll pick out one line of work I particularly like (and thereby miss important references on purpose :). This is the work of Damiano Mazza on redoing classical complexity theory in a higher-order implicit complexity framework. Here are three papers I particularly like:

  1. Church meets Cook and Levin. This re-does the famous Cook-Levin proof (that SAT is NP-complete) in an implicit complexity style. The key idea is that you can use affine lambda terms as a kind of "higher-order circuit", and then approximate regular lambda-terms using them.
  2. This idea is explored further in Non-linearity as the Metric Completion of Linearity, which focuses just on this idea (apparently implicit in Girard).
  3. Most recently at POPL this year, Mazza (with Luc Pellissier and Pierre Vial) showed how most linear intersection type systems arise from a general framework for refinement types introduced by Noam Zeilberger and Paul-André Melliès, in their paper Polyadic Approximations, Fibrations and Intersection Types.

I want to emphasize that this is not comprehensive -- chase the references in these papers!