Institut de Mathématiques de Luminy

Équipe
Logique de la Programmation


Introduction :
Le thème fédérateur de cette équipe est la logique linéaire. Elle comporte également une composante qui s'occupe de théorie des graphes et de théorie des relations.
Les travaux de Gentzen dans les années 1930 ont introduit l'élimination des coupures et l'ont placée au centre de la théorie de la démonstration.
Par la suite, l'isomorphisme de Curry-Howard entre preuves et programmes a considérablement renforcé l'intérêt de l'étude de l'élimination des coupures. Dans cette étude, la logique linéaire est devenue un instrument essentiel qui a permis l'introduction de nouveaux
concepts : réseaux de démonstration et d'interaction, géométrie de l'interaction, logique non commutative. La logique linéaire a également renouvelé les recherches en sémantique dénotationnelle, permettant des rapprochements avec des domaines plus classiques des mathématiques (espaces vectoriels topologiques notamment). Ces dernières années, les phénomènes de focalisation et la notion de formule polarisée ont pris une place centrale, donnant notamment naissance à la ludique, une approche interactive de la logique dans l'esprit des sémantiques de jeux. Enfin, la logique linéaire a donné de nouveaux outils dans le domaine de la recherche de preuves (programmation logique), et introduit de nouveaux problèmes de décidabilité et de complexité.

1 - Élimination des coupures et réseaux de preuves.
2 - Recherche de preuves.
3 - Logique et interaction.
4 - Sémantique dénotationnelle.
5 - Théorie des graphes et des relations.

4.1. Élimination des coupures et réseaux de preuves.

La règle logique de coupure en calcul des séquents peut être vue comme une version du modus ponens. Le théorème d'élimination des coupures de Gentzen énonce que toute formule prouvable avec coupures est aussi prouvable sans coupures (en logique classique, ou intuitionniste), et fournit en plus une méthode effective pour éliminer les coupures d'une preuve, sous la forme d'un système de réécriture. L'extension de cette propriété à travers une "interprétation fonctionnelle" à un système mathématiquement expressif, comme l'arithmétique de Peano du premier ou du second ordre (analyse), permet de prouver la cohérence de ce système et exige donc des principes logiques qui lui sont extérieurs en vertu du second théorème d'incomplétude de Godel. Les preuves d'élimination des coupures (alias normalisation, ou normalisation forte, lorsqu'on parle de lambda-calcul) pour des formalismes comme le système F — dont la normalisation entraîne la cohérence de l'arithmétique de Peano du second ordre — font donc appel à de gros principes logiques au moyen de la méthode de réductibilité.

"Type = Formule" et "Programme = Preuve", c'est ce qu'énonce l'isomorphisme de Curry-Howard entre programmes purement fonctionnels (lambda-termes) et preuves intuitionnistes ; dans cette correspondance, l'évaluation des programmes correspond à l'élimination des coupures. De ce point de vue, le système F, par exemple, peut être vu comme un langage fonctionnel avec types polymorphes (au moyen desquels on peut d'ailleurs représenter de nombreux types de données : entiers, listes, arbres etc.), et la normalisation forte (élimination des coupures) énonce que dans ce langage tous les programmes terminent, éventuellement après un temps de calcul très long. Le système F en effet est très expressif puisque toutes les fonctions prouvablement totales dans l'arithmétique de Peano du second ordre y sont représentables.

Comme elle donne aux règles structurelles (affaiblissement et contraction) un statut logique, par l'introduction de nouveaux connecteurs (exponentielles) et la subdivision des connecteurs usuels (conjonction et disjonction) en deux classes (additive et multiplicative), la logique linéaire (LL) peut être considérée comme un outil pour l'étude de l'élimination des coupures, dont la complexité réside en effet essentiellement dans les règles structurelles. Partant de la constatation que, dans le fragment sans exponentielles, la normalisation forte est triviale, et que LL, au second ordre, est au moins aussi expressif que le système F, il était naturel de chercher des versions "intermédiaires" des exponentielles permettant, typiquement, de ne définir que des fonctions élémentaires, ou mieux, polynomiales. Ce programme a été mené à bien il y a quelques années, avec l'introduction des systèmes ELL et LLL.

La logique linéaire a également permis d'étendre à la logique classique — dont l'élimination des coupures est pourtant "non déterministes" au sens où, à partir d'une même preuve, on peut aboutir à des formes normales complètement différentes selon l'ordre dans lequel on procède — le paradigme de Curry-Howard, notamment à travers les systèmes LC de Girard et LKtq de Danos, Joinet et Schellinx (ces systèmes imposent des choix dans les paires critiques catastrophiques de la logique classique). La notion de formule polarisée (qui est liée à la propriété de focalisation) a permis récemment de reprendre ces études avec de nouveaux outils.

L'un des intérêts de la logique linéaire est d'avoir permis d'introduire les réseaux de démonstrations, qui sont une représentation des preuves réalisant de nombreux quotients par rapport au calcul des séquents ; il arrive souvent en effet dans une preuve que l'ordre entre deux règles n'ait aucune importance, alors que le calcul des séquents impose de le spécifier. Les réseaux ont une élimination des coupures beaucoup plus "asynchrone" que le calcul des séquents, ce qui a notamment suggéré l'introduction d'un nouveau paradigme de calcul, les réseaux d'interaction. Ils permettent aussi d'introduire de nouveaux modes de réduction (élimination des coupures) où il ne s'agit plus de réécrire, mais de se déplacer dans le réseau (qui est un graphe) en suivant certaines règles algébriques prescrites par la géométrie de l'interaction.

La logique linéaire est un outil d'étude des règles structurelles qui leur donne un statut logique. Elle reste cependant commutative, car elle conserve la règle d'échange. La logique non commutative donne un statut logique à cette règle et introduit de nouvelles versions, non commutatives, des connecteurs multiplicatifs.

4.1.1. Temps polynomial.

Yves Lafont a proposé un sous-système très simple de la logique linéaire permettant de "typer" les preuves normalisant en temps polynomial, dans la lignée de la logique linéaire bornée de Girard, Scedrov, et Scott, et la logique linéaire allégée (LLL) de Girard : la logique linéaire douce. Patrick Baillot (admissible cette année comme CR2 au CNRS à Villetaneuse, section 7) a proposé un algorithme d'inférence de types pour un fragment significatif de la logique linéaire allégée (lambda-termes en forme normale et types propositionnels de la logique affine allégée), ce qui montre que le problème de typabilité dans ce cadre est décidable.

4.1.2. Systèmes polarisés et systèmes classiques.

Sous la direction de Laurent Regnier, Olivier Laurent (admissible cette année comme CR2 au CNRS à Paris 7, section 1) a poursuivi son travail de DEA sur les réseaux de preuve polarisés avec connecteurs additifs en définissant une procédure d'élimination des coupures confluente et fortement normalisante et en montrant que l m -calcul (système classique) s'y plonge naturellement. Il a ensuite introduit le système de Logique Linéaire Polarisée (LLP) qui permet d'analyser la logique classique comme la logique linéaire permet d'analyser la logique intuitionniste. Dans la suite de leur travail sur l'analyse linéaire de la logique classique, Myriam Quatrini et Lorenzo Tortora de Falco (Rome) ont montré comment, dans un cadre polarisé et focalisé, les plongements en logique linéaire permettent de définir des sémantiques dénotationnelles pour la logique classique. En collaboration avec Olivier Laurent, ils ont montré l'analogie entre leur approche et celle obtenue par plongement dans la logique linéaire polarisée. Olivier Laurent et Laurent Regnier ont revisité la théorie des traductions dites par continuations de la logique classique dans la logique intuitionniste en les reformulant comme des traductions de LLP dans LL. Ils ont ainsi classifié les traductions par continuations en deux grandes familles : les traductions à la Plotkin et celles à la Krivine.

4.1.3. Réseaux d'interaction.

Sous la direction d'Yves Lafont, Sylvain Lippi a travaillé sur la théorie et la pratique des réseaux d'interaction, réalisant un interprète et introduisant un nouveau codage du lambda-calcul dans ces réseaux.

4.1.4. Logique non commutative.

Paul Ruet a défini avec Roberto Maieli un calcul des séquents focalisé pour la logique non commutative (NL), reposant sur l'existence de partitions d'ordres partiels modulo entropie. Ce travail s'est poursuivi en collaboration avec Jean-Marc Andreoli et Roberto Maieli par une étude du processus de construction de preuves partielles focalisées pour NL. Roberto Maieli a développé un nouveau critère de correction pour les réseaux non commutatifs (dans le cadre multiplicatif), que l'on peut considérer comme la contrepartie non commutative du critère de Danos-Regnier. D'autre part, Virgile Mogbil a trouvé un critère de correction pour ces réseaux, qui est en temps quadratique et permet de traiter les réseaux avec coupures (c'est un critère à base de "contractions").

4.1.5. Systèmes différentiels.

Thomas Ehrhard et Laurent Regnier ont introduit en logique des constructions inspirées du calcul différentiel, comme le suggère le modèle dénotationnel des espaces de Köthe (voir plus loin) étudié par Ehrhard. En particulier, ils ont défini un lambda-calcul différentiel dont ils ont établi les propriétés de base.

4.2. Recherche de preuves.

Il s'agit d'un autre point de vue logique sur le calcul, mis en œuvre par exemple dans le langage Prolog. Dans ce cadre, un programme se présente comme une formule (et non une preuve comme dans Curry-Howard), et l'exécuter revient à en chercher une démonstration dans un certain système logique (d'habitude restreint, pour que la tâche soit faisable). Là aussi, la logique linéaire s'est révélée utile en permettant notamment de dégager le phénomène de focalisation déjà mentionné. Par ailleurs, les différents fragments pertinents de la logique linéaire posent autant de problèmes de décidabilité/complexité pour les questions de prouvabilité correspondantes.

4.2.1. Complexité de fragments de la logique linéaire.

Virgile Mogbil (qui a soutenu sa thèse en janvier 2001) et Tom Krantz ont codé le problème des circuits hamiltoniens en logique linéaire multiplicative, obtenant ainsi une nouvelle preuve de NP-complétude pour ce fragment.

4.2.2. Programmation logique.

Jean-Marc Andreoli a complètement formalisé l'approche "programmation par contraintes" de la recherche de preuves, qui évite de nombreux défauts des approches traditionnelles. Toutefois, les arbres de preuves que l'on construit ainsi contiennent trop de détails inessentiels (ordre des opérations interchangeables), et cela suggère de chercher plutôt à construire des réseaux, ce qui nécessite une théorie des réseaux partiels à laquelle Jean-Marc Andreoli s'est attaqué.

4.3. Logique et interaction.

L'élimination des coupures peut être vue comme une interaction dynamique entre deux preuves, vues comme des stratégies, l'une cherchant à prouver un énoncé, et l'autre à le réfuter. Cette idée était présente dès l'origine dans les œuvres de Gentzen, et a été concrétisée ces dernières années en termes de modèles de jeux, qui ont notamment abouti à des solutions au problème de la "full abstraction" pour PCF. La ludique adopte ce point de vue interactif, fondant la logique sur une notion de "preuves" non typées (les desseins) interagissant par un mécanisme d'élimination des coupures très général.

D'autre part, la géométrie de l'interaction peut aussi être vue comme décrivant les échanges d'informations entre les différentes parties d'un réseau, et de ce point de vue, il n'est pas étonnant qu'elle ait des liens très étroits avec certains modèles de jeux.

4.3.1. Géométrie de l'interaction.

L'extension de la géométrie de l'interaction aux connecteurs additifs a été décrite par Jean-Yves Girard en 1995, Olivier Laurent a proposé une autre solution basée sur la notion de poids additifs (provenant des réseaux de preuve) qui permet d'éviter l'introduction d'un quotient dans l'interprétation.

4.3.2. Ludique.

Jean-Yves Girard a poursuivi le développement de la ludique, théorie qui fonde la logique sur des bases purement interactives. Il a en particulier perfectionné la théorie des desseins et a prouvé des théorèmes de structure et de complétude sur les comportements (ensembles de desseins ayant une propriété de clôture). Il a également écrit un important texte sur le sujet, intitulé Locus Solum, à paraître en juin 2001. Marie-Renée Donnadieu-Fleury et Myriam Quatrini ont exploré l'interprétation des quantificateurs du premier ordre de la logique linéaire en ludique. Elles ont étudié les propriétés d'uniformité susceptibles de garantir un résultat de complétude. Claudia Faggian a approfondi la théorie des desseins, en particulier dans une direction plus "dénotationnelle" et fondée sur la notion de dispute (trace des interactions entre desseins), dont elle a montré, avec Martin Hyland, qu'elle est analogue à la notion de partie dans les jeux. Elle a étudié des extensions non commutatives de la ludique, et a collaboré avec Jean-Marc Andreoli, Roberto Maieli et Paul Ruet sur des applications de cette étude à de nouveaux systèmes de recherche de preuves. L'aspect locatif de la ludique a trouvé des échos dans les travaux menés par René Vestergaard sur les méthodes formelles de preuves équationnelles pour les langages d'ordre supérieur (comme le lambda-calcul), méthodes qu'il a appliquées à la théorie des langages de programmation.

4.3.3. Jeux.

Olivier Laurent a développé un modèle de jeux polarisés pour LLP qui, grâce à l'introduction d'un opérateur de décalage (idée issue de la ludique), possède une véritable dualité entre les deux joueurs. Via les traductions de la logique classique dans LLP, ces jeux fournissent les bases d'un modèle pour les langages fonctionnels avec opérateurs de contrôle aussi bien pour l'appel par nom que pour l'appel par valeur.

4.4. Sémantique dénotationnelle.

Il s'agit ici d'interpréter les preuves comme des morphismes dans certaines catégories dont les objets correspondent aux formules, cette interprétation devant être invariante par élimination des coupures. Dans la "sémantique catégorique", on s'intéresse aux axiomes que ces catégories doivent satisfaire, en fonction des systèmes que l'on souhaite interpréter.

La sémantique dénotationnelle est à l'origine de la logique linéaire, car c'est dans le modèle des espaces cohérents que les exponentielles sont apparues clairement pour la première fois. Les mêmes structures se retrouvent dans les hypercohérences, modèle basé sur la séquentialité et dont les liens avec les jeux déterministes ont été étudiés dans le cadre intuitionnistes.

4.4.1. Hypercohérences.

Sous la direction de Thomas Ehrhard, Pierre Boudes a poursuivi son étude des liens entre hypercohérences et jeux déterministes dans la logique linéaire, se concentrant sur le cas polarisé. Il a notamment été amené à introduire une version non uniforme des hypercohérences.

4.4.2. Sémantique des phases et sémantique dénotationnelle.

Thomas Ehrhard a poursuivi sa collaboration avec Antonio Bucciarelli (Paris 7), étendant aux exponentielles la théorie développée précédemment. Il a ainsi été amené à introduire une version indexée de la logique linéaire propositionnelle, pour laquelle il a étudié le problème de la complétude. Sous sa direction, Alexandra Bruasse-Bac a étendu au second ordre ces constructions, ce qui l'a notamment amenée à revoir, dans un cadre purement relationnel, des notions introduites par Girard en 1986 (sémantique cohérente du système F) et à introduire une version du second ordre de la logique linéaire indexée, dont elle a étudié les propriétés.

4.4.3. Modèles "continus".

Thomas Ehrhard a développé une interprétation de la logique linéaire dans des espaces vectoriels topologiques localement convexes d'un type particulier (les espaces de suites de Köthe). Dans ce cadre, les preuves intuitionnistes sont interprétées par des fonctions analytiques, d'où l'idée d'étendre la logique par des constructions différentielles, cf. son travail avec Laurent Regnier sur le lambda-calcul différentiel. Il a également étudié une version discrète de cette sémantique : les espaces de finitude.

4.4.4. Sémantique catégorique.

Paul Ruet a défini, en collaboration avec Richard Blute (Ottawa) et François Lamarche (Nancy), une notion de modèle catégorique du fragment multiplicatif de NL, les catégories entropiques, stable par élimination des coupures, construit des catégories entropiques à partir d'algèbres de Hopf, et étendu le théorème de reconstruction de Tannaka-Krein au cadre entropique. Laurent Regnier a donné une construction, analogue à celle de la catégorie de Kleisli dans le cas intuitionniste, permettant de produire un modèle catégorique de la logique linéaire polarisée (LLP) à partir d'un modèle de la logique linéaire classique (LL).

4.5. Théorie des graphes et des relations.

Pierre Ille et Gérard Lopez font partie de l'équipe LDP depuis décembre 1996. Leur recherche s'inscrit en théorie des graphes et en théorie des relations dans lesquelles ils s'intéressent aux problèmes de décomposition et de reconstruction. Ces problématiques remontent aux travaux d'Ulam (1960), de Gallai (1967) et de Fraïssé (1970). Durant la période concernée par ce rapport, Pierre Ille s'est plus particulièrement occupé de l'étude de l'indécomposabilité et de la dualité des structures, alors que Gérard Lopez en a étudié les propriétés d'indéformabilité.

Last update : September 22, 2001, EL.