English

10 Pages

Gain access to the library to view online

__
Learn more
__

Description

Niveau: Supérieur

April 8, 2005 — Final version, appearing in Proceedings of LICS 2005 Constructing free Boolean categories Franc¸ois Lamarche Loria & INRIA-Lorraine Projet Calligramme 615, rue du Jardin Botanique 54602 Villers-les-Nancy — France Lutz Straßburger Universitat des Saarlandes Informatik — Programmiersysteme Postfach 15 11 50 66041 Saarbrucken — Germany Abstract By Boolean category we mean something which is to a Boolean algebra what a category is to a poset. We pro- pose an axiomatic system for Boolean categories, which is different in several respects from the ones proposed re- cently. In particular everything is done from the start in a *-autonomous category and not in a weakly distributive one, which simplifies issues like the Mix rule. An important axiom, which is introduced later, is a “graphical” condi- tion, which is closely related to denotational semantics and the Geometry of Interaction. Then we show that a previ- ously constructed category of proof nets is the free “graphi- cal” Boolean category in our sense. This validates our cat- egorical axiomatization with respect to a real-life example. Another important aspect of this work is that we do not as- sume a-priori the existence of units in the *-autonomous categories we use. This has some retroactive interest for the semantics of linear logic, and is motivated by the properties of our example with respect to units.

April 8, 2005 — Final version, appearing in Proceedings of LICS 2005 Constructing free Boolean categories Franc¸ois Lamarche Loria & INRIA-Lorraine Projet Calligramme 615, rue du Jardin Botanique 54602 Villers-les-Nancy — France Lutz Straßburger Universitat des Saarlandes Informatik — Programmiersysteme Postfach 15 11 50 66041 Saarbrucken — Germany Abstract By Boolean category we mean something which is to a Boolean algebra what a category is to a poset. We pro- pose an axiomatic system for Boolean categories, which is different in several respects from the ones proposed re- cently. In particular everything is done from the start in a *-autonomous category and not in a weakly distributive one, which simplifies issues like the Mix rule. An important axiom, which is introduced later, is a “graphical” condi- tion, which is closely related to denotational semantics and the Geometry of Interaction. Then we show that a previ- ously constructed category of proof nets is the free “graphi- cal” Boolean category in our sense. This validates our cat- egorical axiomatization with respect to a real-life example. Another important aspect of this work is that we do not as- sume a-priori the existence of units in the *-autonomous categories we use. This has some retroactive interest for the semantics of linear logic, and is motivated by the properties of our example with respect to units.

- both
- let now
- direction natural
- qqqq qqqq
- yyy yyyy
- htt ?

Subjects

Informations

Published by | chaeh |

Reads | 9 |

Language | English |

Report a problem