My graduate student Harley Eades and I have recently completed a draft paper on normalization for a type theory called Stratified System F (SSF), using the idea of hereditary substitution. SSF was originally studied by Daniel Leivant and then Leivant and Norman Danner. See papers like “Finitely Stratified Polymorphism” (sorry, subscription link), or “Stratified Polymorphism and Primitive Recursion”, for example. SSF is like System F, except that every type is kinded at a certain level (just a natural number). So universal types look like , where is a natural number. The universal quantification itself has a level higher than and than the level of the body (this is a minor change from Leivant’s system, where the quantification just has to have level greater than )). The critical restriction is that when you instantiate a universal type, you must do so at a level at or below the level declared for the variable. This greatly restricts the complexity of the functions one can write: indeed, the set of functions representable in SSF is much smaller than the set of primitive recursive functions, which in turn is much, much smaller than the set representable in System F.
In our paper, we show how the idea of hereditary substitution can be used to prove (weak) normalization for SSF. Hereditary substitution was first brought to the attention of the computational logic community (as I mentioned in an earlier post) by the paper “A concurrent logical framework I: Judgments and properties”, by K. Watkins et al. The idea with hereditary substitution is to reduce certain redexes that might be created during substitution. Reducing those redexes might in general require recursive calls to hereditary substitution. The crucial insight is that in such cases, the type of the substituted term is smaller than it was for the original call to hereditary substitution. So reducing created redexes only requires recursive calls at smaller type, and hence hereditary substitution is terminating.
The paper works through the details of developing a proof of normalization based on this idea of hereditary substitution for SSF. SSF’s level restriction on instantiation makes it possible to define a well-founded ordering in which all (kindable) instances of a (kindable) universal type are smaller than the universal type.