April Final version appearing in Proceedings of LICS

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.

• both


• let now


• direction natural


• qqqq qqqq


• yyy yyyy


• htt ?