A BRICS Mini-Course
June 3 and 4, 1997
Lectures by
Philip Scott
Department of Mathematics, University of Ottawa, Canada
In this series of talks I describe a new, categorical approach to normalization in typed lambda-calculus and related theories. In a recent paper by D. Cubric, P. Dybjer, and P. J. Scott, we show how to solve the word problem for simply typed lambda beta eta-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is P-category theory, a version of ordinary category theory where each homset is equipped with a partial equivalence relation. The part of P-category theory we develop here is constructive; this permits extracting a normalization algorithm.
Our methods have intriguing analogues to the Joyal-Gordon-Power-Street techniques for proving coherence in various structured (bi-)categories and are also closely related to Berger and Schwichtenberg's method for normalizing lambda-terms. The technique is an example of normalization by intuitionistic model construction, a method going back to Martin-Löf. The general idea is to prove normalization by first interpreting a term in a suitable model and then map this interpretation back to the normal form of the term. By working in an intuitionistic framework one ensures that the normalization function thus obtained is an algorithm.
The same general technique was used later by Berger and Schwichtenberg to construct a normalization algorithm for simply typed lambda beta eta-calculus, by inverting the interpretation function into the set-theoretic model. Recently, Altenkirch, Hofmann, and Streicher gave a categorical version of the proof of U. Berger and H. Schwichtenberg (``An inverse to the evaluation functional for typed lambda-calculus'', Proceedings of the 6th Annual IEEE Symposium of Logic in Computer Science, 1991, pp. 203-211.), based on a syntactically-inspired gluing method. Our work continues the categorical analysis, the crucial difference being our use of P-category theory, which enables us to solve the word problem for cccs by purely (enriched) categorical means. To show the robustness of our method, we show how to extend it to certain lambda-theories and beyond.