Adjoint Rewriting

Abstract

This thesis is about rewriting in the typed lambda-calculus. Traditional categorical models of typed lambda-calculus use concepts such as functor, adjunction and algebra to model type constructors and their associated introduction and elimination rules, with the natural categorical equations inherent in these structures providing an equational theory for lambda-terms. One then seeks a rewrite relation which, by transforming terms into canonical forms, provides a decision procedure for this equational theory. Unfortunately the rewrite relations which have been proposed, apart from for the most simple of calculi, either generate the full equational theory but contain no decision procedure, or contain a decision procedure but only for a sub-theory of that required.

Our proposal is to unify the semantics and reduction theory of the typed lambda-calculus by generalising the notion of model from categorical structures based on term equality to categorical structures based on term reduction. This is accomplished via the addition of a pre-order to each of the hom-sets of the category which will be used to reflect the reduction of one term to another. Canonical rewrite relations, whose associated theory matches that suggested by the traditional semantics, may then be derived from the natural categorical constructions on these ordered categories.

Rewrite relations derived in this fashion typically consist of a contractive beta-rewrite rule and an expansionary eta-rewrite rule for each type constructor. Although confluent, the presence of expansionary eta-rewrite rules means the rewrite relation is not strongly normalising and so cannot in itself be used as the basis of a decision procedure. Instead, decidability of the equational theory is proved by a variety of term rewriting techniques which will necessarily vary from calculus to calculus. These techniques are developed in three case studies; the simply typed lambda-calculus with unit, product and exponential types; the linear lambda-calculus containing the tensor from linear logic; and the bicartesian closed calculus obtained by adding coproducts to the simply typed lambda-calculus.