PROGRAM

Preliminary Program

Abstracts of the talks:


Les réseaux de preuve selon Christian Retoré et après : inférence profonde et algorithmique des graphes (Lê Thành Dũng (Tito) Nguyễn)
Dans sa thèse, Christian introduit la logique pomset au moyen d'un système de réseaux de preuve. Motivée par des considérations sémantiques et combinatoires très naturelles, cette logique ne semblait néanmoins pas se prêter à être exprimée en calcul des séquents. Ceci a poussé Alessio Guglielmi à développer l'inférence profonde – un paradigme plus permissif que les séquents – pour y formuler le système BV. Conjecturalement, BV avait vocation à être équivalent à la logique pomset, fournissant ainsi pour cette dernière un formalisme déductif (basé sur des règles d'inférence, contrairement aux réseaux de preuve). Si toute formule prouvable par BV l'est aussi en logique pomset, Lutz Straßburger et moi avons récemment réfuté la réciproque, restée ouverte pendant deux décennies. C'est en fait un autre travail de Christian – reliant les réseaux de preuves aux couplages parfaits, et ainsi à la théorie des graphes « mainstream » – qui nous a mené à découvrir une distinction inattendue entre ces deux logiques du point de vue de la complexité algorithmique, et nous a donc motivés à chercher un contre-exemple explicite à la conjecture. Une interprétation de ce contre-exemple vient d'être proposée par Aleks Kissinger et Will Simmons dans le cadre de leur théorie des structures causales, qui débouche sur une extension conservative de la logique pomset.

Cographes et hypercohérences (Thomas Ehrhard)
Les cographes sont des graphes qui ont joué un rôle important dans le travail de Christian Rétoré sur les réseaux de preuves, car on peut les voir comme des arbres avec deux sortes de noeuds internes (tenseur et par). Je montrerai comment ils apparaissent aussi très naturellement dans les espaces d'hypercohérence, un modèle de la logique linéaire où tous les morphismes "du 1er ordre" sont séquentiels au sens de Vuillemin.


Composition et multitypage de grammaires catégorielles abstraites  (Sylvain Pogodalla,  travail réalisé avec Philippe de Groote et Pierre Ludmann)
Les grammaires catégorielles abstraites ont la particularité d'offrir différents paradigmes de composition de grammaires, qui peuvent être utilisés pour différents types de modélisation : contrôle des structures admissibles d'analyse, codage des relations entre forme et surface, etc. Nous discuterons différentes difficultés liées à la composition et introduirons la notion de multitypage pour les grammaires catégorielles abstraites et de leur composition, premier pas vers le développement de grammaires catégorielles abstraites pondérées.

Les Grammaires Minimalistes, de la syntaxe à la sémantique (Maxime Amblard) 

Les grammaires minimalistes, introduites par Ed. Stabler, encodent le programme minimaliste de N. Chomsky. Il s’agit d’une formalisation calculable, motivée par des propriétés syntaxiques. Une interprétation des propriétés utilisées par ces grammaires, dans les grammaires catégorielles a permis de conserver les structures dérivées et de leur donner une interprétation logique, au travers de l’isomorphisme de Curry-Howard. Cette idée trouve son origine dans la collaboration entre Christian Retoré et Alain Lecomte. Nous reviendrons sur le fonctionnement de ces grammaires, et discuterons comment les structures dérivées permettent de rendre compte de la sémantique des langues naturelles.


Machines universelles et combinateurs d’interaction (Yves Lafont)

Les réseaux d’interaction ont été introduits par l’auteur dès 1990, puis les combinateurs d’interaction font l’objet de sa première publication majeure en 1997. On voit facilement qu’une machine de Turing correspond à un système d’interaction où chaque réseau est de dimension 1, c’est -à-dire une chaîne de cellules. Les systèmes d’interactions sont donc un modèle universel du calcul, mais on peut démontrer un résultat beaucoup plus intéressant !


Les combinateurs d’interaction sont les 3 symboles d'un système d’interaction très simple, avec seulement 6 règles, fortement inspiré par les réseaux de preuve de Girard, mais il n’est pas nécessaire de connaître la logique linéaire pour en comprendre les mécanismes. La principale propriété de ce système est qu’il est universel parmi les systèmes d’interaction, en un sens fort : la simulation d’un système quelconque est fidèle, c’est-à-dire que chaque cellule correspond à un réseau de combinateurs, et chaque règle à une suite d’interactions entre combinateurs : en particulier, le degré de parallélisme et la complexité algorithmique sont strictement préservés. La démonstration de ce théorème est inspirée par le code génétique en biologie : le système d’interaction que l’on veut simuler définit un réseau de combinateurs qui est constamment dupliqué (ou effacé) pour être présent partout dans le réseau de combinateurs qui simule nos calculs.