Séminaire Logique et Interactions

Le premier article construisant une géométrie de l'interaction ("Multiplicatives" de J.-Y. Girard) est issu d'une réflexion autour du critères de correction des réseaux multiplicatifs. Par la suite, plusieurs modèles de GdI basés sur les algèbres d'opérateurs ont été élaborés, introduisant au passage de nouveaux outils: déterminants pour "compter les cycles", notion de "dialecte"... Les graphes d'interaction présentés la semaine dernière montrent que l'on peut utiliser ces outils dans un cadre plus "combinatoire" utilisant des objets finis pour représenter les (para)preuves: des graphes pondérés. Ceci ouvre la possibilité de calculer si deux (para)preuves sont orthogonales, possibilité que l'on peut tenter d'exploiter pour définir des critères de correction pour divers systèmes logiques, notamment MALL.

Les graphes d'interaction généralisent la toute première géométrie de l'interaction définie par Girard dans l'article “Multiplicatives”. En remplaçant les permutations (utilisées dans “Multiplicatives”) par des graphes orientés pondérés, il est possible de définir une notion d'orthogonalité en comptant les cycles apparaissant lors du branchement de deux graphes. Il est alors possible d'obtenir une géométrie de l'interaction pour MALL dépendant de la fonction qui mesure les cycles. Après avoir défini cette géométrie de l'interaction, je montrerai comment il est possible d'obtenir un modèle dénotationnel de MALL et une notion de vérité à partir de ce modèle. Enfin, je montrerai qu'en choisissant judicieusement la fonction de mesure, il est possible d'obtenir soit la géométrie de l'interaction dans sa version ancienne (GdI1, avec une orthogonalité basée sur la nilpotence), soit une version combinatoire de la GdI5 de Girard. Ceci permet donc de donner une interprétation géométrique à l'orthogonalité de Girard basée sur le déterminant, et de relier cette nouvelle construction à celles plus anciennes basées sur la nilpotence.

Les variantes de la logique linéaire pour la complexité implicite, comme ELL, LLL, SLL, ont permis de caractériser plusieurs classes de complexité: P, la classe Elem du temps élémentaire (tour d'exponentielles de hauteur bornée), PSPACE? Dans ces différents systèmes les modalités exponentielles sont définies par des règles plus ou moins faibles, qui limitent le pouvoir d'expression de la logique. Les comparaisons des systèmes entre eux restent cependant difficiles.

Nous proposons une autre démarche consistant à caractériser dans une même logique plusieurs classes de complexité, en considérant pour chacune un type différent. Pour cela nous nous intéressons à la logique linéaire élémentaire ELL, introduite par Girard, un sous-système simple de la logique linéaire permettant initialement de caractériser la classe Elem. Nous considérons son extension avec des points fixes de types et montrons que malgré sa simplicité, cette logique permet de caractériser la classe P et les différents niveaux d'une hiérarchie de classes de complexité de temps exponentiel.

In this talk, we present a counterexample to a conjecture of Rozoy and Thiagarajan from 1991 (called also the nice labeling problem) asserting that any (coherent) event structure with finite degree admits a labeling with a finite number of labels, or equivalently, that there exists a function f : N → N such that an event structure with degree ≤ n admits a labeling with at most f(n) labels. Our counterexample is based on the Burling’s construction from 1965 of 3-dimensional box hypergraphs with clique number 2 and arbitrarily large chromatic numbers and the bijection between domains of event structures and median graphs (alias 1-skeletons of CAT(0) cube complexes) established by Barthélemy and Constantin in 1993.

In the second part of the talk, we will outline the proof that the contact graph of a 2-dimensional CAT(0) cube complex X of maximum degree d can be coloured with at most q(d)= Md^15 colours, for a fixed constant M. This implies that X (and the associated median graph) isometrically embeds in the Cartesian product of at most q(d) trees, and that the event structure whose domain is X admits a nice labeling with q(d) labels. This second result is based on a join paper with Mark Hagen.

Les « systèmes d'interaction » étaient à l'origine un moyen de représenter une notion de « jeux » en théorie des types. On obtient de cette manière une catégorie de jeux et de simulations qui modélise la logique linéaire différentielle. De manière assez surprenante, la dynamique ne joue aucun rôle dans la définition de composition des stratégies !

Cette notion de jeux existe sous des noms différents : « containers » (Ghani, Altenkirch, Hancock, …) ou « foncteurs polynomiaux » (Hyland, Kock, Gambino, …). Ce qui change ici est la notion de morphisme, plus générale que dans la littérature existante.

Après une petite introduction, je montrerai les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirai ensuite le modèle de (D)ILL en insistant sur l'interprétation en termes de jeux et les similarités formelles avec le modèle « dégénéré » des transformateurs de prédicats.

Je ne ferai probablement aucune preuve, mais je mentionnerai quand même l'outil important, à savoir le langage interne des catégories localement cartésiennes fermées (càd la théorie des types dépendants)…

Le λ-calcul avec constructeurs est une extension du λ-calcul avec un mécanisme de filtrage (pattern matching). Le filtrage à la ML y est décomposé en deux étapes: une simple analyse de cas sur des constantes, et une règle surprenante de commutation entre l'application et la construction de filtrage.

Dans cet exposé, nous définirons une notion générique de modèle catégorique pour ce calcul. Nous construirons ensuite un modèle particulier, le modèle syntaxique (dans la catégorie des PERs), et nous en déduirons un résultat de complétude.

Enfin nous montrerons comment construire des modèles non syntaxiques du λ-calcul avec constructeurs en partant d'une traduction CPS. On obtiendra ainsi des modeles par continuation pour le calcul.