Skip to main content Accessibility help
×
Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-06T01:04:42.787Z Has data issue: false hasContentIssue false

Modelling reduction in confluent categories

Published online by Cambridge University Press:  24 September 2009

M. P. Fourman
Affiliation:
University of Edinburgh
P. T. Johnstone
Affiliation:
University of Cambridge
A. M. Pitts
Affiliation:
University of Cambridge
Get access

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 Science
Proceedings of the London Mathematical Society Symposium, Durham 1991
, pp. 143 - 162
Publisher: Cambridge University Press
Print publication year: 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×