1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Wednesday 15 November, 11am
Peter Dybjer (Chalmers and Newton Inst.)
The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this talk I introduce n alternative approach to normalization, which bypasses the reduction relation and instead focuses on the normalization function, that is, the function which maps a term into its normal form. We work in an intuitionistic metalanguage, and characterize a normalization function as an algorithm which picks a canonical representative from the equivalence class of convertible terms. Hence we also get a decision algorithm for convertibility.
Such a normalization function can be sometimes be constructed by building an appropriate model and a function "quote" which inverts the nterpretation function. The normalization function is then obtained by composing the quote function with the interpretation function. I also discuss how to get simple proofs of consistency and of the property that constructors are one-to-one, which usully are obtained as corollaries of Church-Rosser and normalization in the traditional sense.
I plan to illustrate the approach by two examples. The first is a proof of normalization of binary words with respect to associativity and unit laws by an interpretation in a monoid of endofunctions. The second example shows how a glueing model (closely related to the glueing construction used in category theory) gives rise to a normalization algorithm for a combinatory formulation of Godel System T. I then show how the method extends in a straightforward way when we add cartesian products and disjoint unions (full intuitionistic propositional logic under a Curry-Howard interpretation) and transfinite inductive types such as the Brouwer ordinals.
If time permits I will also make some comments about the connection between reduction-free normalization and categorical proofs of coherence, and about the relevance of "constructive category theory" (category theory developed in the metalanguage of intuitionistic type theory) in this context.