Ordinals in Type Theory
If a type system for functional programming
ensures that evaluation of properly typed expressions terminates,
and the type system is decidable,
then the type system is necessarily incomplete. This is an
expression of the unsolvability of the halting problem.
Very roughly, one can measure the incompleteness of such a type system
with a countable ordinal -- the supremum of those that can be expressed with
properly typed expressions. This has been extensively studied for almost
70 years, since Gentzen.
Together with P. Hancock and A. Setzer we have been analysing
the ordinals of systems such as Martin-Lof Type Theory with
one universe. While the ordinal of this system is known (P. Aczel),
the proofs that it is the correct ordinal are very indirect.
We have been working on a direct construction of this
ordinal, and introduces the notion of lenses for this purpose.
This has been presented as an invited lecture at the CSL meeting, August
1997.
We also intend to develop a natural representation
of ordinals as iterative sets (which model Aczel's constructive version of
Zermelo-Fraenkel Set Theory following an idea of Herman Jervell.
Last modified: Thu May 28 13:01:00 MET DST 1998