Logical relation categories and lambda calculi.

Abstract

An aspect of programming languages is the study of the operational semantics, which, in the case of a lambda calculus, is based on a directed form of equational reasoning called reduction. In computer science terminology, reduction may be regarded as a form of symbolic evaluation. It models a sequential computation process step by step. The crucial properties for a rewriting system are confluence, also called the Church-Rosser property and termination, the (Strong) normalization property, respectively. These are studied in depth in Chapter 2 and 6. The problem whether all $\lambda$-terms satisfy termination corresponds to the halting problem. From a different point of view, studying the problem of both Church-Rosser and strong normalization corresponds to, in a particular field, studying the word problem. The notion of categories is familiar to mathematicians as a branch of algebra. It has been developed quite rapidly in less than 40 years. In particular, recently more and more computer scientists are using categories for their own purposes. It is the connection between categories and $\lambda$-calculi that interests computer scientists. This connection is a thread that goes through the whole thesis. (Abstract shortened by UMI.)