SMF

Sémantique catégorielle de la logique linéaire

Categorical Semantics of Linear Logic

Paul-André MELLIÈS
Sémantique catégorielle de la logique linéaire
  • Consulter un extrait
  •  
                
  • Année : 2009
  • Tome : 27
  • Format : Électronique
  • Langue de l'ouvrage :
    Anglais
  • Class. Math. : 03-02, 03B05, 03B10, 03B15, 03B20, 03B22, 03B40, 03B45, 03B47, 03B70, 03F03, 03F05, 03F07, 03F52, 03G30, 18A15, 18A40, 18C20, 18C50, 18D05, 18D10, 18D15, 18D25, 91A05, 91A20, 91A40, 91A80
  • Pages : 1-196

La théorie de la démonstration est issue d'une histoire courte et tumultueuse, construite en marge des mathématiques traditionnelles. Aussi, son langage reste souvent idiosyncratique : calcul des séquents, élimination des coupures, propriété de la sous-formule, etc. Dans cet article, nous avons voulu guider le lecteur à travers la thématique, en lui traçant un chemin progressif et raisonné, qui part des mécanismes symboliques de l'élimination des coupures, pour aboutir à leur transcription algébrique en diagrammes de cohérence dans les catégories monoïdales. Cette promenade spirituelle au point de convergence de l'algèbre et de la linguistique est ardue parfois, mais aussi pleine d'attraits : car à ce jour, aucune langue (formelle ou informelle) n'a été autant étudiée par les mathématiciens que la langue des démonstrations logiques.

Proof theory is the result of a short and tumultuous history, developed on the periphery of mainstream mathematics. Hence, its language remains often idiosyncratic : sequent calculus, cut-elimination, subformula property, etc. This survey is designed to guide the novice reader and the itinerant mathematician along a smooth and consistent path, investigating the symbolic mechanisms of cut-elimination, and their algebraic transcription as coherence diagrams in categories with structure. This spiritual journey at the meeting point of linguistic and algebra is demanding at times, but a rewarding experience : to date, no language (either formal or informal) has been studied by mathematicians as thoroughly as the language of proofs.

Théorie de la preuve, calcul séquent, élimination par coupe, sémantique catégorielle, logique linéaire, catégories monoïdales, catégories $\ast $-autonomes, catégories linéairement distributives, catégories de dialogue, diagrammes de chaînes, boîtes fonctorielles, 2-catégories, foncteurs monoïdaux, adjonctions monoïdales, espaces de cohérence, sémantiques de jeu.
Proof theory, sequent calculus, cut-elimination, categorical semantics, linear logic, monoidal categories, $\ast $-autonomous categories, linearly distributive categories, dialogue categories, string diagrams, functorial boxes, 2-categories, monoidal functors, monoidal adjunctions, coherence spaces, game semantics