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
Weakly distributive 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
There are many situations in logic, theoretical computer science, and category theory where two binary operations—one thought of as a (tensor) “product”, the other a “sum”—play a key role, such as in distributive categories and in -autonomous categories. (One can regard these as essentially the AND/OR of traditional logic and the TIMES/PAR of (multiplicative) linear logic, respectively.) In the latter example, however, the distributivity one often finds is conspicuously absent: in this paper we study a “linearisation” of distributivity that is present in this context. We show that this weak distributivity is precisely what is needed to model Gentzen's cut rule (in the absence of other structural rules), and show how it can be strengthened in two natural ways, one to generate full distributivity, and the other to generate -autonomous categories.
Introduction
There are many situations in logic, theoretical computer science, and category theory where two binary operations, “tensor products” (though one may be a “sum”), play a key role. The multiplicative fragment of linear logic is a particularly interesting example as it is a Gentzen style sequent calculus in which the structural rules of contraction, thinning, and (sometimes) exchange are dropped. The fact that these rules are omitted considerably simplifies the derivation of the cut elimination theorem. Furthermore, the proof theory of this fragment is interesting and known [Se89] to correspond to *-autonomous categories as introduced by Ban in [Ba79].
In the study of categories with two tensor products one usually assumes a distributivity condition, particularly in the case when one of these is either the product or sum.
- Type
- Chapter
- Information
- Applications of Categories in Computer ScienceProceedings of the London Mathematical Society Symposium, Durham 1991, pp. 45 - 65Publisher: Cambridge University PressPrint publication year: 1992
- 10
- Cited by