Constructing free Boolean categories

François Lamarche 1 Lutz Straßburger 2, 3
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : By Boolean category we mean something which is to a Boolean algebra what a category is to a poset. We propose an axiomatic system for Boolean categories, which differs in several respects from the one given very recently by Fuehrmann 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 denotational semantics and the Geometry of Interaction. Then we show that the proof net model presented in TLCA2005 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. This has some retroactive interest for the semantics of linear logic, and is motivated by the properties of our TLCA proof nets with respect to units.
Type de document :
Communication dans un congrès
20th Annual IEEE Symposium on Logic in Computer Science - LICS 2005, May 2005, Chicago/USA, United States. pp.209- 218, 2005, 〈10.1109/LICS.2005.13〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00012296
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 30 novembre 2012 - 11:31:42
Dernière modification le : jeudi 12 avril 2018 - 01:46:39
Document(s) archivé(s) le : vendredi 1 mars 2013 - 02:20:10

Fichier

FreeBool.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

François Lamarche, Lutz Straßburger. Constructing free Boolean categories. 20th Annual IEEE Symposium on Logic in Computer Science - LICS 2005, May 2005, Chicago/USA, United States. pp.209- 218, 2005, 〈10.1109/LICS.2005.13〉. 〈hal-00012296v2〉

Partager

Métriques

Consultations de la notice

441

Téléchargements de fichiers

210