March This is an expanded version of the LICS'05 submission Mistakes have been corrected and the relative emphasis of axioms has changed but the claims are strictly identical

Niveau: Supérieur
March 12, 2005 — This is an expanded version of the LICS'05 submission. Mistakes have been corrected and the relative emphasis of axioms has changed, but the claims are strictly identical. 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, similar to but differing in several respects from the one given very recently by Fuhrmann and Pym. In particular everything is done from the start in a *-autonomous category and not a linear distributive one, which simplifies issues like the Mix rule. An important axiom, which is introduced later, is a “graphical” condition, which is closely related to denota- tional semantics and the Geometry of Interaction. Then we show that a previously constructed category of proof nets is the free “graphical” Boolean category in our sense. This validates our categorical axiomatization with respect to a real-life example. Another important aspect of this work is that we do not assume a-priori the existence of units in the *-autonomous categories we use.

• both


• let now


• autonomous categories


• ural transformation πx


• direction natural


• qq qq


• preserves both


• definition let


• htt ?