## Adjoint Rewriting

**Neil Ghani**
*Abstract:* This thesis is about rewriting in the typed
lambda-calculus. Traditional categorical models of typed
lambda-calculus u se 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.

**ECS-LFCS-95-339**, December 1995.

This report is available in the following formats:

Previous |

Index |

Next