Page d'accueil
Sommaire

[ Présentation générale ] [ Relations internationales ] [ Devenir des doctorants ] [ Élimination des coupures et réseaux de preuves ]
[ Recherche de preuves ] [ Logique et interaction ] [ Géométrie du calcul ] [ Logique philosophique ] [ Théorie des graphes et des relations ]
[ Algorithmique pour la sûreté de fonctionnement ] [ Programme de recherche ]

Institut de Mathématiques de Luminy

Logique de la programmation
Rapport scientifique 1999-2002

Présentation générale

Le thème fédérateur de cette équipe est la théorie de la démonstration, et plus particulièrement les liens que cette théorie entretient avec l'informatique. Elle comporte également une composante qui s'occupe de théorie des graphes et de théorie des relations et a intégré Antoine Rauzy (ancien membre du LaBRI) au printemps 2001, qui s'occupe d’algorithmique pour la sûreté de fonctionnement. Signalons enfin le statut particulier de Jean-Marc Andreoli, directeur de recherche associé au CNRS et membre de notre équipe depuis 1998, qui est par ailleurs membre du centre de recherche Xerox européen, situé à Grenoble (XRCE).

Contexte scientifique.

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 en particulier). 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é. Mais l’étude du calcul développée au sein de notre équipe exploite également d’autres approches, plus éloignées de la théorie de la démonstration, catégoriques et homologiques notamment.

Relations internationales

De mai 1998 à octobre 2002, l’équipe, en la personne de Laurent Regnier, a été coordinatrice d’un projet européen Training and Mobility of Researchers (TMR) intitulé "Linear Logic in Computer Science". Ce projet regroupait les principaux laboratoires européens actifs dans ce domaine : deux sites français (Marseille et Paris), deux britanniques (Edimbourg et Cambridge), deux italiens (Bologne et Rome) et un portugais (Lisbonne). Il a favorisé, voire même créé, des liens scientifiques fructueux entre ces divers sites, au moyen du financement d’une dizaine d’années de stages post-doctoraux et de l’organisation régulière de rencontres scientifiques. Il a également organisé une école d’été en août 2000 aux Açores, qui a rassemblé une quarantaine d’étudiants de toutes nationalités.

Dans le cadre de l’opération "Trimestres Thématiques" de l’IML, l’équipe a co-organisé avec le Laboratoire d’Informatique de Marseille la série de rencontres Logique et Interaction (LI2002) qui se sont tenues au CIRM durant tout le mois de février 2002. Ces rencontres ont réuni une centaine de chercheurs internationaux parmi lesquels se retrouvaient souvent les meilleurs spécialistes mondiaux des domaines concernés. Elles étaient organisées autour de trois grands thèmes : complexité algorithmique, géométrie du calcul, logique et vérification. Les deux premières semaines constituaient une école destinée aux doctorants et aux chercheurs. On pourra consulter le programme de ces rencontres sur le site web :

http://iml.univ-mrs.fr/~li2002.

En coopération avec Michele Abrusci de l’université de Rome 3, l’équipe a mis en place un réseau de formation doctorale, intitulé "Logique mathématique et informatique théorique", entre l’Université de la Méditerranée et l’Université de Rome 3, qui a reçu le financement de l’Université Franco-Italienne pour l’année 2002-2003.

L’objectif de ce réseau est de faciliter la mobilité des doctorants en leur permettant de suivre des cours et d’effectuer des séjours de recherche dans un autre laboratoire que celui où se déroule leur thèse, et plus généralement d’approfondir les collaborations universitaires entre les deux communautés scientifiques en favorisant les échanges d’enseignants, de chercheurs et de personnel administratif. L’équipe a invité de nombreux chercheurs de classe internationale durant la période couverte par ce rapport, tant sur des postes CNRS qu’universitaires. Le volume de ces invitations a été, en moyenne, de six mois par an.

Devenir des doctorants

Une bonne part des étudiants ayant préparé et soutenu leur thèse au sein de notre équipe ont trouvé assez rapidement des postes d’enseignants-chercheurs ou de chercheurs.

Patrick Baillot a soutenu sa thèse en janvier 1999 (directeur : Jean-Yves Girard) et obtenu un poste de CR2 au CNRS au Laboratoire d’Informatique de Paris Nord (LIPN, Paris 13 et CNRS) en 2001.

Alexandra Bruasse-Bac a soutenu sa thèse en décembre 2001 (directeur : Jean-Yves Girard et Thomas Ehrhard) et a obtenu un poste de maître de conférences en 2002 à l’École Supérieure d’Ingénieurs de Luminy et au Laboratoire d’Informatique Fondamentale (Université de la Méditerranée, Université de Provence et CNRS).

Olivier Laurent a soutenu sa thèse en mars 2002 (directeurs : Jean-Yves Girard et Laurent Regnier) et obtenu un poste de CR2 au CNRS dans le laboratoire Preuves, Programmes et Systèmes (Paris 7 et CNRS).

Virgile Mogbil a soutenu sa thèse en janvier 2001 (directeur : Yves Lafont) et obtenu un poste de maître de conférences à Paris 13 (LIPN).

Voici la situation des étudiants sans poste fixe, ayant soutenu leur thèse ou étant sur le point de la soutenir.

Pierre Boudes doit soutenir sa thèse en décembre 2002 (directeur : Thomas Ehrhard) et est actuellement ATER à l’Université de la Méditerranée.

Claudia Faggian a soutenu sa thèse en avril 2002 (directeur : Jean-Yves Girard) et est actuellement en stage post-doctoral à l’université de Cambridge.

Sylvain Lippi a soutenu sa thèse en juin 2002 (directeur : Yves Lafont). Il est actuellement ATER au Centre de Mathématiques et d’Informatique (Université de Provence).

Les autres thèses actuellement en cours au sein de l’équipe sont celles d’Alaeddine Ben Rhouma (directeur : Thomas Ehrhard), Christophe Gaubert (Paul Ruet), Jean-Christophe Godin (Yves Lafont), Pierre Hyvernat (Jean-Yves Girard et Thierry Coquand de l’université Chalmers à Göteborg), Luca Paolini (Jean-Yves Girard et Giuseppe Rosolini de l’université de Gênes) et Samuel Tronçon (Jean-Yves Girard et Pierre Livet de l’Université de Provence).

Enfin, sur la période considérée, nous avons dû déplorer deux abandons de thèse : Thomas Krantz et Nuno Barreiro.

É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 Gödel. 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é entrepris, il y a quelques années, avec l’introduction des systèmes ELL et LLL, et se poursuit actuellement. La logique linéaire a également permis d’étendre le paradigme de Curry-Howard à la logique classique – dont l’élimination des coupures est pourtant "non déterministe" 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 – 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émonstration, 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.

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, et exactement celles-là, 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 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. Il a également étudié la sémantique dénotationnelle de LLL et ELL au moyen des espaces cohérents stratifiés qu’il a introduits. Durant son séjour parmi nous (de décembre 2001 à juin 2002), Terui Kazushige a étudié une extension de LLL, à savoir le lambda-calcul affine en espace polynomial, qui capture exactement cette classe de complexité et qui permet de simuler un certain nombre de constructions naturelles en théorie des fonctions récursives. Il a également étudié la complexité de la réduction dans la logique linéaire multiplicative et dans la logique linéaire multiplicative-additive. Dans ce cas en particulier, il a montré que la réduction est P-complète au moyen d’un codage des circuits booléens.

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

Olivier Laurent 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 le l m -calcul (système de logique 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.

Géométrie des réseaux de preuves.

Christophe Gaubert a prolongé les travaux de François Métayer où les réseaux de preuves sont vus comme des surfaces, et où l’on s’intéresse aux rapports entre la complexité topologique et la règle d’échange du calcul des séquents. Il a montré notamment que la surface associée à un réseau est celle de complexité minimale pour y plonger le réseau sans croisement. Il a travaillé sur les réseaux de la logique linéaire additive, notamment les réseaux à poids de Girard, en essayant d’adapter des résultats portant sur les réseaux multiplicatifs : critère homologique de correction, modules…

 

Réseaux d’interaction.

Sylvain Lippi a travaillé sur la théorie et la pratique des réseaux d’interaction. Il a réalisé pour ces réseaux un interprète possédant une interface agréable. Sur un plan théorique, il a obtenu des résultats généraux sur la duplication et l’effacement dans les réseaux et a introduit un nouveau codage du lambda-calcul dans ces réseaux. Cela lui a permis de donner une version de la machine de Krivine graphique, définie en six règles d’interaction. Il a étendu ces constructions au lambda-calcul avec continuations (qui correspond à la logique classique). Il a également obtenu une preuve graphique de la confluence forte de la réduction spinale. Il a soutenu sa thèse sur ce thème en juin 2002.

Logique non commutative.

Paul Ruet a défini avec Roberto Maieli (en stage post-doctoral TMR chez nous d’octobre 2000 à septembre 2001) 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").

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) et des espaces de finitude étudiés par Ehrhard. En particulier, ils ont défini un lambda-calcul différentiel dont ils ont établi les propriétés de base : confluence, normalisation forte dans le cas typé. Ils ont analysé dans ce cadre le développement de Taylor et l’ont relié à la réduction linéaire de tête (la procédure d’évaluation des lambda-termes implémentée par la machine de Krivine). Ce travail établit un lien étroit entre dérivation, au sens de l’analyse, et substitution linéaire, au sens du lambda-calcul et de la logique linéaire. Alaeddine Ben Rhouma commence une thèse sur ce sujet.

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.

Complexité de fragments de la logique linéaire.

Virgile Mogbil 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.

Mécanismes de construction de preuves.

Jean-Marc Andreoli a complètement formalisé l’approche "programmation par contraintes" de la recherche de preuves, en corrigeant 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 qu’il a mise au point et a appliquée à la modélisation de mécanismes "middleware".

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 dans des modèles de jeux, qui ont notamment abouti à des solutions au problème de la "complétude pleine" pour PCF, un langage de programmation fonctionnel. La ludique adopte ce point de vue interactif : elle fonde la logique sur une notion de "preuves" polarisées mais non typées (les desseins) interagissant par un mécanise 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.

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.

Ludique.

Jean-Yves Girard a développé la ludique, théorie qui fonde la logique sur des bases purement interactives. L’objet de base est le dessein qu’on peut voir comme une "(para-)preuve normale non typée", dont la structure est en couches alternées positif/négatif, conformément à ce que nous a appris la focalisation. Ces preuves ne portent pas sur des formules, mais sur des occurrences (ce qui reste des formules quand on a oublié le superflu…) et sont donc localisées. L’interaction fondamentale est celle d’une "preuve" et d’une "contre-preuve", qui peut diverger ou converger sur le démon, la para-preuve par excellence (on peut difficilement admettre d’avoir à la fois une preuve d’une formule et de sa négation, d’où le "para"). Cette dualité est le cœur de la ludique. Elle permet de définir des ensembles "réflexifs" (égaux à leurs bi-duaux) de desseins, les comportements, qui correspondent aux formules logiques. La théorie développée par Girard porte essentiellement sur les comportements, leur structure et leurs propriétés de complétude, et propose de dépasser la traditionnelle distinction syntaxe/sémantique en mettant en place un cadre nouveau où des phénomènes informatiques connus, comme le sous-typage, devraient recevoir un traitement logique satisfaisant. Girard a écrit en particulier un important texte sur le sujet, intitulé Locus Solum.

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 et ont analysé le cas du second ordre avec Claudia Faggian. Celle-ci a par ailleurs 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 ainsi pu donner un nouveau point de vue, plus dans l’esprit de la théorie de la démonstration, sur certains concepts de base de sémantique des jeux (vues et innocence, notamment). Elle a introduit des outils pour travailler de manière effective avec les notions de la ludique : desseins (programmes) et comportements (types). 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 (en stage post-doctoral TMR dans notre équipe durant l’année 2000-2001) 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.

On retrouve également un caractère locatif important dans le travail de Jean-Marc Andreoli qui propose une approche axiomatique du traitement des règles structurelles dans toute une famille générique de systèmes logiques dérivés de la logique linéaire, et dont la Logique Non Commutative est une instance.

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. Pierre Boudes a exploité ce cadre sémantique polarisé pour définir une notion de jeux "à bords" (i.e. avec une notion de partie achevée) dans le but de dégager des liens entre jeux et hypercohérences dans l’esprit des résultats de collapse extensionnel qu’Ehrhard avait obtenus en 1993-94.

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.

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, qui permet de construire des modèles dénotationnels de la logique linéaire à partir d’espaces de phases d’une forme particulière. Cela a abouti à la construction de nouveaux modèles concrets non uniformes de la logique linéaire, analogues aux espaces cohérents. Au cours de ce travail, il a é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. 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. Elle a également défini une nouvelle interprétation des exponentielles dans le cadre des modèles dénotationnels construits sur des espaces de phases. Ce travail a fait l’objet de sa thèse, soutenue en décembre 2001.

Hypercohérences.

Pierre Boudes a trouvé des versions non uniformes des hypercohérences où les exponentielles sont interprétées au moyen de constructions à base de multi-ensembles (prise en compte des multiplicités). Ces nouvelles interprétations se démarquent nettement de celles que l’on obtient par la sémantique des phases car elles préservent une propriété fondamentale de déterminisme des interprétations uniformes. Ce travail lui a permis ensuite de mettre à jour de nouvelles interprétations uniformes qui montrent que la situation, dans le domaine des modèles séquentiels "extensionnels", est plus complexe que ce que l’on pensait (réfutation de la "conjecture de Longley"). Il a également généralisé au cas des hypercohérences infinies une construction introduite par Ehrhard et qui permet, dans certaines conditions, de produire un jeu à bord à partir d’une hypercohérence.

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.

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. Il a 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).

Géométrie du calcul

La géométrie du calcul est un nouveau domaine mathématique issu de plusieurs approches telles que la théorie combinatoire des groupes, les catégories, la réécriture, et la topologie algébrique. On étudie les calculs d’un point de vue géométrique et algébrique, et non plus seulement d’un point de vue logique et algorithmique. Parmi les précurseurs de cette théorie, on peut citer Albert Burroni (problèmes de mot en dimension supérieure) et Craig Squier (invariants homologiques de la réécriture).

Homologie des groupes gaussiens.

L’algorithme de redressement de Thurston permet de construire des résolutions libres et de calculer explicitement l’homologie de certains groupes tels que les groupes de tresses, dans la lignée des travaux d’Anick, Squier, et Kobayashi sur l’homologie des monoïdes associés à des systèmes de réécriture complets. Yves Lafont a travaillé sur ce thème avec Patrick Dehornoy (université de Caen), introduisant une nouvelle approche combinatoire permettant de calculer l’homologie des groupes localement gaussiens.

Théorie algébrique des circuits.

Les circuits booléens sont utilisés pour représenter des programmes sur des données de taille fixe. Les circuits booléens réversibles et les circuits booléens quantiques ont été introduits pour modéliser certains aspects physiques du calcul. Ces notions sont essentielles en théorie de la complexité, mais une véritable théorie mathématique est certainement nécessaire pour progresser dans ce domaine. On pourrait s’inspirer, par exemple, des récents développements de la théorie des nœuds. En suivant les idées de Burroni, Yves Lafont considère les portes logiques comme des générateurs pour une théorie algébrique avec deux compositions (catégorie monoïdale) et il s’intéresse aux relations satisfaites par ces générateurs. Pour cela, il introduit des formes canoniques et des systèmes de réécriture. Jusqu’à présent, il a surtout étudié le "cas basique" et la "cas linéaire", mais il espère que ces méthodes permettront d’obtenir des présentations par générateurs et relations pour le "cas classique" (réversible) et le "cas quantique" (unitaire).

Logique philosophique

Il s’agit ici d’une tentative de renouer des liens, que nous estimons un peu distendus, entre logique mathématique moderne et logique philosophique. Concrètement, Jean-Yves Girard et Pierre Livet (université de Provence) co-dirigent la thèse de Samuel Tronçon depuis octobre 2000. Celui-ci étudie la caractérisation philosophique des différents systèmes de théorie de la démonstration, particulièrement ceux apparus depuis les années 1960 : théorie des types, déduction naturelle, logique linéaire, jeux, ludique… Il a aussi organisé trois colloques réunissant des chercheurs autour de la philosophie de la logique : philosophes, logiciens, mathématiciens. Il travaille activement à la collaboration scientifique entre quatre unités reconnues : l’équipe Logique De la Programmation de l’IML, l’équipe "Logica Lineare" à Rome 3, le Centre d’Épistémologie et d’Ergologie Comparatives, le département de Philosophie de Paris 1.

Théorie des graphes et des relations

La recherche de Pierre Ille et de Gérard Lopez s’inscrit en théorie des graphes et en théorie des relations dans lesquelles ils s’intéressent plus particulièrement 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). Le problème général de reconstruction en théorie des relations peut être posé de la façon suivante. …tant données deux relations R et R’ définies sur le même ensemble, est-ce-que l’isomorphie entre certaines restrictions de R et de R’ entraîne l’isomorphie entre R et R’ ? Le premier résultat significatif en reconstruction des relations est dû à Lopez qui a établi en 1978 que les relations binaires sont reconstructibles à partir de leurs restrictions de cardinal 6. Ce théorème ayant clos le problème de reconstruction des relations par leurs restrictions de "petite taille", Ille et Lopez ont poursuivi leurs travaux en reconstruisant les relations par des restrictions de grande taille. Dernièrement, Boudabbous et Lopez ont caractérisé les relations non reconstructibles à partir des restrictions d’une certaine taille. Dans la plupart des cas, afin de reconstruire une relation, on essaie de la décomposer de la façon suivante. Un intervalle d’une relation ou d’un graphe est un ensemble de sommets tel que chaque élément de son complémentaire est relié de la même manière à tous ses éléments. Autrement dit, on peut décomposer un graphe en considérant un intervalle comme un sommet. Gallai a montré en 1967 que des décompositions successives de ce type aboutissent à des graphes complets, vides ou indécomposables, c’est-à-dire, des graphes dont tous les intervalles sont triviaux. La difficulté réside alors dans l’étude de la structure des graphes indécomposables, qui constitue l’un des principaux thèmes de recherche d’Ille. Par exemple, Boudabbous, Dammak et Ille viennent de caractériser les tournois indécomposables dont tous les sous-tournois stricts et indécomposables sont autoduaux.

Algorithmique pour la sûreté de fonctionnement

Antoine Rauzy travaille sur la sûreté de fonctionnement de système, c’est-à-dire l’ensemble des méthodes qui permettent d’évaluer le risque et les conséquences du risque dans des installations industrielles sensibles (centrales nucléaires, industries chimiques et pétrolières, avionique, transport…). Pour évaluer le risque, les ingénieurs font des modèles et emploient donc des formalismes de description. Ces derniers sont principalement des formalismes Booléens ou des formalismes états/transitions (automates d’états finis, réseaux de Petri…). Une fois l’installation décrite par un modèle, il faut se servir de ce modèle pour évaluer les quantités (en général probabilistes) qui donnent une mesure du risque (probabilité ou fréquence des accidents/incidents) et de ses conséquences (gravité, impact sur l’environnement, impact économique…).

Ce processus soulève deux problèmes, liés entre eux :

Son travail depuis 10 ans (et pour les 10 ans à venir) consiste à avancer dans les deux directions : d’une part par la mise au point de formalismes de description et de méthodologies de modélisation, d’autre part par la mise au point d’un corpus d’algorithmes et d’heuristiques permettant de repousser aussi loin que possible les limites de l’explosion combinatoire. Ce type de recherches implique de s’attaquer à des problèmes issus de la pratique industrielle. Cela n’aurait en effet aucun sens de travailler sur des problèmes artificiels car on n’aurait aucune garantie d’applicabilité aux problèmes réels. Cela implique aussi un très gros travail d’ingénierie pour développer les outils, les rendre utilisables par des ingénieurs (incluant la fastidieuse rédaction de manuels), mettre en place les protocoles expérimentaux, mettre au point les heuristiques…

Sur la période concernée par ce rapport, Antoine Rauzy s’est attaché essentiellement à des tâches de programmation, sur deux projets :

Programme de recherche

Voici quelques thèmes de recherche que certains membres de notre équipe se proposent pour ces prochaines années, ou sont actuellement en train de développer.

Attention : cette liste est purement indicative et ne prétend pas à l'exhaustivité.

Jean-Yves Girard.

Approfondissement et systématisation du lien récemment découvert entre logique et mécanique quantique.

Yves Lafont.

L'article intitulé "Towards an Algebraic Theory of Algebraic Circuits" sera prochainement soumis à publication. Même si les résultats sont prometteurs, on est encore assez loin des buts visés : présentations par générateurs et relations pour le calcul booléen réversible et pour le calcul booléen quantique ; applications à la théorie de la complexité algorithmique. Yves Lafont et son nouveau thésard Jean-Christophe Godin vont continuer à étudier la question, mais il serait souhaitable de constituer un groupe de travail autour de ce thème.

Un autre aspect de la géométrie du calcul est le sujet du livre "Problème du mot et géométrie de la réécriture" en cours de rédaction. Lafont y présente deux jolis résultats : le théorème de Novikov (indécidabilité du problème du mot pour les groupes), et le théorème de Squier (invariants homologiques de la réécriture). La récente théorie des groupes Gaussiens pourrait être intégrée à cet ouvrage du type "cours spécialisé de 3ème cycle".

Marie-Renée Donnadieu-Fleury et Myriam Quatrini.

Poursuite de l'étude de la quantification du 1er ordre en ludique. Parallèlement, étude de la possibilité d'utiliser les objets de la ludique pour représenter des problèmes relatifs à la gestion et à la mise à jour des bases de données.

Thomas Ehrhard et Laurent Regnier.

Poursuite de l'étude du lambda-calcul différentiel, et en particulier de la signification opérationnelle de la formule de Taylor. Ehrhard continuera d'étudier la sémantique dénotationnelle de ce système et son thésard Ben Rhouma s'intéressera en particulier à la sémantique des opérateurs de point fixe et du lambda-calcul différentiel non typés qui semble poser des questions intéressantes.

Pierre Ille.

En théorie des graphes, Ille aborde des problèmes de combinatoire finie et infinie. D'une part, avec Boudabbous, il vient d'obtenir un procédé de construction des graphes infinis, indécomposables et critiques en introduisant une généralisation des opérations classiques de quotient et de somme lexicographique. D'autre part, avec Hahn et Woodrow, il étudie la structure des graphes idempotents pour le produit lexicographique au moyen de leur arbre de décomposition. Concernant les structures finies, avec Rampon, il essaie de caractériser les ordres partiels admettant un nombre donné de types d'isomorphie de leurs sous-ordres obtenus en enlevant un seul sommet.

Page d'accueil
Sommaire