Modelling reduction in confluent categories
C. Barry Jay · Cambridge University Press eBooks · 1992
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 λ-calculus these constructions yield confluently cartesian closed categories. A third such model, in which the call rule is used to interpret β-reduction, is also given. Introduction One of the cornerstones of programming language semantics is the correspondence between simply-typed λ-calculi and cartesian closed categories established by Lambek and Scott [LS86]. It provides a clean algebraic semantics for λ-terms, which helps us to reason effectively about the values of programs. Of equal interest to the implementer, however, is the reduction process which computes these values, i.e. the operational semantics. One of the most satisfying approaches to date is Plotkin's structural operational semantics [Plo75, Plo81] which uses a sequent calculus to describe the reduction process and provide a rigorous specification for computation. In spite of their separate virtues, it is difficult to relate the logic (of operational semantics) to the categorical algebra (of denotational semantics); the usual approach, using computational adequacy, is rather unwieldy.