BRICS · Contents · Programme · Registration

**A BRICS Mini-Course**

**June 3 and 4, 1997**

**Lectures by
Philip Scott
**

**
**

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.

### Tuesday June 3, 1997, 10:15-12:00 in Colloquium B4

### Wednesday June 4, 1997, 10:15-12:00 in Colloquium B4