Sujet de mémoire de recherche pour un master en informatique

Graphes de démonstration
pour la logique linéaire partiellement commutative

Christian Retoré ( retore@labri.fr / 05 40 00 38 72 )

(autres sujets)

Proposition

Les réseaux de démonstration sont des graphes qui représentent fidèlement les preuves de la logique linéaire.[1]

Dans certains cas, on réussit à obtenir une caractérisation simple des graphes qui correspodnent à des preuves, avec des outils standard de la théorie des graphes. C'est en particulier le cas avec des graphes munis d'un couplage parfait pour la logique linéaire commutative (LL) où les preuves sont les graphes dont tous les cycles élémentaires alternants contiennent une corde. [2] C'est aussi le cas pour le calcul de Lambek (L), variante non commutative de la logique linéaire.[3]

Il existe une logique partiellement commutative, qui inclut les connecteurs commutatifs (LL) et les non commutatifs (L), qui peut être classique ou intutionniste. Les contextes sont dans ce cas des ordres série-parallèles de formules. [4,5] Le calcul classique a été bien étudié et des réseaux de démonstration existent.[6]

Par contre, pour le calcul intutionniste, qui autorise une gestion plus souple des contextes, on ne connaît pas encore de réseaux, simplement un calcul des séquents [5] et un système de déduction naturelle [7] qui fonctionnent bien (normalisation). Trouver des réseaux de démonstration dans le style de [2,3] pour la logique linéaire partiellement commutative est l'objet de ce mémoire.

On pourra s'inspirer du critère algébrique de [8].


Observations

Ce sujet est relativement risqué. Bien qu'il soit presque assuré de trouver une solution, puisqu'on propose ce sujet, on ne peut en être sûr tant que le résultat n'est pas établi. En labsence du résultat attendu, une synthèse de tous les résultats similaires fera un mémoire honnête. En revanche, si l'étudiant encadré y arrive, alors il s'agit d'un joli résultat, et donc d'un très bon master recherche.

Ce sujet peut être poursuivi en un doctorat d'informatique que ce soit en essayant de démontrer une conjecture analogue (1993) pour le calcul ordonné (pomset logic ou le calcul des structures de Guglielmi) soit en exploitant ce type de logique mixte pour créer des grammaires catégorielles modélisant assez souplement la syntaxe et la sémantique du langage naturel.

Bibliographie

[1] Girard, J.-Y. : Linear Logic, Theoretical Computer Science, 50:1, pp. 1-102, 1987.

[2] Christian Retoré Handsome proof nets: perfect matchings and cographs. Theoretical Computer Science. 294(3), 2003, pages 473–488 http://hal.inria.fr/docs/00/07/30/20/PDF/RR-3652.pdf

[3] Sylvain Pogodalla and Christian Retoré (2004) Handsome Non-Commutative Proof-Nets: perfect matchings, series-parallel orders and Hamiltonian circuits INRIA RR-5409 Work presented at Categorial grammars 2004, LIRMM, Montpellier, juin 2004. To appear in Journal of Applied Logic http://hal.inria.fr/docs/00/07/12/48/PDF/RR-5409.pdf

[4] Philippe de Groote (1996) Partially commutative linear logic: sequent calculus and phase semantics. In Vito Michele Abrusci and Claudia Casadio, editors, Third Roma Workshop: Proofs and Linguistics Categories -- Applications of Logic to the analysis and implementation of Natural Language, pages 199--208. Bologna:CLUEB, 1996.

[5] Christian Retoré (2004). A description of the non-sequential execution of petri nets in partially commutative linear logic.In Jan van Eijck, Vincent van Oostrom, and Albert Visser, editors, Logic Colloquium 99, Lecture Notes in Logic, pages 152--181. ASL and A.K. Peters, 2004. http://hal.inria.fr/docs/00/07/22/99/PDF/RR-4288.pdf

[6] V. Michele Abrusci and Paul Ruet (1999). Non-commutative logic I: The multiplicative fragment. Annals of pure and applied logic, 101(1):29--64, 1999.

[7] Maxime Amblard et Christian Retoré Natural Deduction and Normalisation For Partially Commutative Linear Logic and Lambek Calculus with product (with M. Amblard) Computation and Logic in the Real World (Computing in Europe 2007) In S. B. Cooper and T. F. Kent and B. Löwe and A. Sorbi (eds) Quaderni del Dipartimento di Scienze Matematiche e Informatiche "Roberto Magari" ID487 pages 28--35. http://www.mat.unisi.it/~sorbi/Proceedings.pdf

[8] Philippe de Groote (1999). An algebraic correctness criterion for intuitionistic multiplicative proof-nets Theoretical Computer Science 224(1-2) pp. 115-134.