samuel mimram (seminar)

Une approche algébrique des sémantiques interactives
Samuel Mimram
CEA

Les sémantiques de jeux décrivent le comportement interactif des preuves en interprétant les formules comme des jeux sur lesquels les preuves induisent des stratégies. Dans ce travail, nous introduisons une telle sémantique afin de capturer les dépendances induites par les quantifications en logique propositionnelle du premier ordre. L'une des principales difficultés qui doit être surmontée durant l'élaboration de telles sémantique est la caractérisation des stratégies définissables, qui sont les stratégies qui se comportent comme des preuves. La façon habituelle de procéder consiste à restreindre le modèle aux stratégies satisfaisant certaines conditions combinatoires subtiles, telles que l'innocence, dont la préservation par composition est souvent difficile à montrer.

Ici, nous présentons une méthodologie originale alternative, qui nécessite de combiner des outils avancés de sémantique des jeux, de théorie de la réécriture et d'algèbre catégorique. Nous introduisons une présentation diagrammatique de la catégorie monoidale des stratégies définissables du modèle, par générateurs et relations : ces stratégies peuvent être générées à partir d'un ensemble fini de stratégies atomiques et l'égalité entre stratégies peut être finiment axiomatisée, cette structure équationnelle correspondant à une variant polarisée de la notion de bigèbre. Ce travail relie ainsi algèbre et sémantique dénotationnelles afin de révéler la structure des dépendances induites par les quantificateurs du premier ordre, et pose les bases d'une étude automatisée de l'analyse de la causalité dans les langages de programmation.

Nous évoquerons la façon dont ce travail peut être appliqué à la synthèse et à la vérification de processeurs.