Now we are corcerning about the termination properties of reduction
on the typed -
calculus. As we all know, reductions of some untyped
-terms, such
as
and
, may diverge. Does it happen too on typed
-terms? We are so lucky to get an answer:``NO''. We are pretty
safe in reductions on typed
-terms, which is stated formally in
following theorems. These properties may help us in understanding the
difference between the typed and untyped
-calculus.
We can present the last theorem in a more formal way to give us a better
understanding. First introducing a binary relation on terms:
Now, we can rephrase the theorem in the following way:
or
Above theorems are stated in order of difficulty of their proofs.
The proof to the first theorem will be presented in the next lecture,
while the others will be too difficult to be fit into a class.
(See CN92 for proofs.) Since we
know that terms such as ,
, and
can result in
infinite reduction sequence, thus what these theorems tell us is that
we cannot type these terms.
Next time, we will continue our discussion on termination properties first, and then, introducing a new type constructor, Cartesion Product, into our Type family.