Remarks on Subject Reduction

During the last class we discussed Subject-Reduction. Specifically, if where is a Type, and we know that reduces to some then we claim that as well. We note a couple of things about this result. First of all, finding the type of is a polynomial time result (Constable and Ravi think it is in fact linear, whereas the type inference algorithm for the Milner let statement as done in Gunter is exponential time complete!!).

We also note that since is a reduced version of , it's easier to type then it is to type . This suggests a strategy of reducing our terms until they're as simple as possible, and then typing them. In practice, of course, this doesn't make any sense for a compiler. Essentially it means run the program, and then type it. So static typing is generally used, instead.

It would be nice if knowing the type of could tell us something about the type of . The statement of the Subject-Reduction Theorem is: We'd now like to consider the converse of this theorem, namely: If this were true, then more terms would be typable, e.g. those containing the Y combinator. However, with a little thought an immediate counter-example presents itself. Suppose is some untypable term, but reducing it to throws out the untypable subterm. As an example, let This has an untypable subterm, However, when we reduce this, as we have shown previously, we get which is of type . This has a definite type. Thus, the converse fails.

We can, however, view the failure of the converse in a somewhat positive light. We will look at this as an opportunity to extend our way of typing subterms by employing some wider typing rules. We modify the typing rules by adding the rule: The consequences of this are theoretically very interesting. We get a new class of -calculus which has not been very well studied in the literature. Call this new calculus and the old -calculus . We can add the and combinators to (think of letrec in ML) and still have total computable functions. This is a very interesting possibility. One should note that if we were to add and to , they would destroy the strong termination (strong normalization) properties. Exercise: Prove that adding the Y combinator and the above typing rule destroys the strong normalization result.