Skip navigation

[This post is by Tianyi Liang.] In the last week’s graduate seminar, we discussed Harley Eades’ proof of normalization of a predicative polymorphic type theory called Stratified System F. Harley’s proof uses the idea of hereditary substitutions, due to Watkins and Pfenning.

Before the introduction and also in the previous seminar, we discussed some technique for proving normalization of simply typed and polymorphic lambda calculi, which is also known as the Tait-Girard reducibility method. In simply typed lambda calculi, the terms are defined as x | \lambda x:\phi . t | t t , while in Stratified System F, we have an extended term definition with type variable abstraction, which is \Lambda X : K . t , and term instantiation, which is t\{ \Phi \} . In the simply typed one, types are defined as X | \Phi \rightarrow \Phi, while in Stratified System F, they are extended with \forall X : K . \Phi. Also, in Stratified System F, a kinding relation is introduced, which relates a level to a type with respect to some context, using algorithmic type/kind-checking rules.

To better understand the quantified types, we discussed its convenience: in the simply typed language, we can assign many similar types to the same term, for example: \lambda x . x : nat \rightarrow nat , \lambda x . x : T \rightarrow T , and so on. With quantification, we may assign the single type \forall X . X \rightarrow X instead. Another example regarding type variable abstraction is that: a term t is defined as follows: t = \Lambda X: *_2 . \lambda y : X . y, of type \forall X : *_2 . (X \rightarrow X). Thus, t \{ \Phi \} =_\beta \lambda y : \Phi . y : \Phi \rightarrow \Phi. We also discussed the well-formedness of contexts. An example is given: y:X is not well-formed, while X : *_2 . y : X is well-formed.

There are two differences in the kind-checking rules between Harley and Leivant. One is in the variable rule, Harley added the assumption: p \leq q; the other is in the forall-type rule, Harley changed the kind level from max(p,q+1) to max(p,q)+1.

In our discussion, we put more focus on the proof of lemma 12, which is substitution for the interpretation of types. The lemma itself shows the interpretations of types are closed under substitutions. The hereditary substitution function lies at the heart of the substitution lemma. In fact the substitution function, denoted [t_2/x]^\Phi t_1 where terms t_1 and t_2, type \Phi, and free variable x are inputs, can be constructively extracted from the proof of the substitution lemma. The hereditary substitution function for Stratified System F is terminating.

Harley defined the interpretation of types on normal terms and then extended this definition to non-normal terms. Also, Harley mentioned that his definition of the interpretation of types is equivalent to the following: n in [| \Phi |]_\Gamma iff \Gamma \vdash n : T, where n is a normal term, \Gamma is a context, and \Phi is a type. The harder thing to observe is that in Harley’s definition of the interpretation of types he didn’t explicitly state that \Gamma is well-formed, but this is inferred from the fact that his definition is restricted to kindable types. Thus, by lemma 1 in his paper, we can infer that \Gamma must be well-formed, which proves that the above definition is equivalent.

Then, we discussed the main result, the type soundness for the interpretation of types: If \Gamma \vdash t : \Phi then t \in [| \Phi |]_\Gamma. Theorem 13 shows the type-checking rules are sound with respect to the interpretation of types. We remark that by the extension of the interpretation of types if typing is sound with respect to the interpretation of types then we can conclude that Stratified System F is in fact normalizing.

Since the definition of the hereditary substitution function is so central to the proof, Vilhelm mentioned a style of formalized proof where the lambda expressions are defined as a data typed indexed by their type, and the type system enforces that all functions on them are type preserving. The hope would be that anything we write would be looking like the “extracted substitution function” in the paper, but with the types indexed enough that it itself expresses the proof. However, it wouldn’t be quite so easy, because in addition to the fact that the hereditary function is type preserving, we also need to know that it acts like several reduction steps, and that if there is no redex in the argument there will be no redex in the result. Tracking all that through indexed types seems a bit much, so a formalized development may still need to have some external proofs about it.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: