Modelling Reduction in Confluent Categories

Abstract

Rewriting systems can be modelled categorically by representing terms as morphisms and reduction by an order on the homsets. Confluence of the system, and hence of the homset orders, yields a confluent category. Collapsing these hom-orders, so that a term is identified with their reducts, and in particular any normal form it might have, then yields a denotational semantics. Confluent functors, natural transformations and adjunctions can also be defined, so that on passing to the denotations they yield the usual notions. Two general ways of constructing such models are given. In the first objects are types and morphisms are terms, with substitution represented by equality. The second has contexts for objects and declarations for morphisms, with the call mechanism represented by a reduction. When applied to the simply-typed $\lambda$-calculus these constructions yield confluently cartesian closed categories. A third such model, in which the call rule is used to interpret $\beta$-reduction, is also given.