Book contents
- Frontmatter
- Contents
- Preface
- Miscellaneous Frontmatter
- Computational comonads and intensional semantics
- Weakly distributive categories
- Sequentiality and full abstraction
- Remarks on algebraically compact categories
- Dinaturality for free
- Simply typed and untyped lambda calculus revisited
- Modelling reduction in confluent categories
- On clubs and data-type constructors
- Penrose diagrams and 2-dimensional rewriting
- Strong monads, algebras and fixed points
- Semantics of local variables
- Using fibrations to understand subtypes
- Reasoning about sequential functions via logical relations
- I-categories and duality
- Geometric theories and databases
- Partial products, bagdomains and hyperlocal toposes
Modelling reduction in confluent categories
Published online by Cambridge University Press: 24 September 2009
- Frontmatter
- Contents
- Preface
- Miscellaneous Frontmatter
- Computational comonads and intensional semantics
- Weakly distributive categories
- Sequentiality and full abstraction
- Remarks on algebraically compact categories
- Dinaturality for free
- Simply typed and untyped lambda calculus revisited
- Modelling reduction in confluent categories
- On clubs and data-type constructors
- Penrose diagrams and 2-dimensional rewriting
- Strong monads, algebras and fixed points
- Semantics of local variables
- Using fibrations to understand subtypes
- Reasoning about sequential functions via logical relations
- I-categories and duality
- Geometric theories and databases
- Partial products, bagdomains and hyperlocal toposes
Summary
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 λ-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.
- Type
- Chapter
- Information
- Applications of Categories in Computer ScienceProceedings of the London Mathematical Society Symposium, Durham 1991, pp. 143 - 162Publisher: Cambridge University PressPrint publication year: 1992
- 4
- Cited by