LIPN

Responsable : Christophe FOUQUERÉ

Au cours des quatre dernières années, l’équipe Logique, Calcul et Raisonnement a connu une restructuration, conformément aux recommandations du comité d‘évaluation du CNRS. Après le départ de Philippe Balbiani en septembre 2000, les recherches se sont recentrées autour de trois domaines principaux : la logique linéaire (et ses raffinements/extensions) et diverses applications en informatique ; les spécifications de systèmes et l’aide à la modélisation avec des applications notamment aux systèmes dynamiques et distribués et aux bases de données ; la combinatoire algébrique et la mise au point d’outils pour le développement et l’analyse d’algorithmes en physique mathématique. Ces recherches sont complétées par celles effectuées dans deux autres domaines : la représentation et le raisonnement temporel ; l’analyse de documents du web (en collaboration avec le Laboratoire de Linguistique Informatique).

Des recrutements ont eu lieu dans les trois domaines principaux : pour le thème logique linéaire, Patrick Baillot a été recruté CR2 en 2001, Virgile Mogbil (2002) et Jean-Vincent Loddo (2003) maîtres de conférence ; pour le thème spécifications, Laure Petrucci a été recrutée en 2003 sur un poste de professeur ; pour le thème combinatoire, Frédéric Toumazet a été recruté maître de conférences en 2001. Depuis mai 2002, l’équipe est dirigée par Christophe Fouqueré, en remplacement de Jacqueline Vauzeilles.

Thème : Logique linéaire, réseaux de preuves et applications (Patrick Baillot, Rémi Baudot, Denis Béchet, Jacqueline Castaing, Pascal Coupey, Christophe Fouqueré, Jean-Vincent Loddo, Marcel Masseron, Virgile Mogbil, Jacqueline Vauzeilles).

La logique linéaire, introduite par Jean-Yves Girard en 1985, est un raffinement à la fois des logiques classique et intuitionniste, qui a permis en particulier de donner un statut logique aux opérations de duplication et d’effacement d’hypothèses. Depuis son introduction, la logique linéaire a eu un rôle sans cesse croissant dans l’étude et la compréhension de divers problèmes d’informatique : aspects opérationnels des langages de programmation et de leurs stratégies, sémantique des langages séquentiels et concurrents, complexité calculatoire.

Tous les travaux de ce thème ont en commun l’étude ou l’utilisation de la logique linéaire (ou de ses dérivées : raffinements, extensions, …) en vue d’applications en informatique. Ces travaux ont été effectués pour la plupart dans le cadre du projet européen Training and Mobility of Researchers “Linear Logic in Computer Science“, terminé en 2002. Les travaux sont poursuivis actuellement dans divers projets : action spécifique "Mobilité" (2002-2003), projet MathStic "Sémantique des langages de programmation" (2001-2002), et deux ACI débutant en 2003 GeoCAL ("Géométrie du calcul") et CRISS ("Contrôle de ressources et d'interférences pour systèmes synchrones").

Outre les arrivées mentionnées ci-dessus, signalons que Rémi Baudot a soutenu sa thèse (décembre 2000) avant d’obtenir un poste en entreprise et que Denis Béchet a été en détachement à l’INRIA (IRISA) de 2001 à 2003.

Logique linéaire, réseaux de preuves et réseaux d’interaction

Les réseaux de preuves sont une représentation graphique des preuves de la logique linéaire. Ils ont inspiré les réseaux d'interaction (dus à Yves Lafont) qui sont un modèle de calcul basé sur la réécriture de graphes. Les travaux, menés au LIPN, concernent le mécanisme d'évaluation des réseaux de preuves et d'interaction et leurs transformations.

On a étudié l'idée qui consiste à simuler un système d'interaction par un système plus simple (à la façon des machines universelles dans le cadre des machines de Turing) [D. Bechet, RTA'2001]

On a par ailleurs étudié les propriétés des réseaux de preuves et surtout de morceaux de réseaux appelés modules. Cette notion de module intervient dans de nombreux travaux actuels, et est particulièrement intéressante dans le cadre de la linguistique “computationnelle“.

Toutefois, jusqu'à présent, l'utilisation des modules dans des applications pratiques butait sur un problème de représentation. En effet, personne n'avait encore pu caractériser leur interface par des objets facilement utilisables (la représentation était soit un ensemble de partitions des points de l'interface du module - donc des ensembles d'ensembles - soit le réseau entier du module qui est de taille non bornée par rapport au nombre de points de l'interface et donc arbitrairement complexe). On a donné une représentation sous forme de réseaux dont la taille en nombre de nœuds est linéaire par rapport au nombre de points de l'interface et dont le nombre d'arêtes est quadratique par rapport à ce même nombre. Ainsi cette représentation enlève la limitation sur l'utilisation des modules. Ce travail a été exposé à un colloque du TMR “Linear Logic in Computer Science“. Ce résultat a été un préliminaire pour le développement d’un analyseur syntaxique du langage naturel. Ce travail a été présenté durant le détachement de son auteur auprès de l’INRIA à IWPT’2003 (non listé dans les publications du laboratoire).

Comme extension intéressante de la notion de réseaux de preuve et de modules, on s’intéresse aussi au problème de la complexité de la recherche de preuve dans le fragment multiplicatif et cyclique de la logique linéaire. Mati Pentus a démontré en juin 2003 que ce fragment est NP-complet. Toutefois, nous pensons que certaines sous-classes de ce problème sont polynomiales. En particulier, l’utilisation de ce fragment pour la linguistique computationnelle est très particulière : le lexique et donc les modules associés sont connus. La recherche de preuve a donc lieu dans un contexte qui n’est pas quelconque. Nous cherchons par conséquent à définit des sous-classes ayant une complexité polynomiale par des restrictions sur la taille, l’ordre ou la forme des formules.

Programmation logique en logique linéaire

L'exécution d'un programme logique consiste en la réduction d'un but au moyen d'applications par résolution de clauses. Ce paradigme appliqué aux clauses de Horn sous-tend le langage Prolog. Andreoli l'a étendu au langage complet de la logique linéaire (commutative), dont la théorie de la démonstration offre un cadre approprié. Nous avons développé nos travaux dans deux directions : d'une part extension à la non-commutativité, d'autre part programmation avec résolution implicite.

La logique non commutative (NL) a été introduite en 1997 par Paul Ruet et Michele Abrusci ; c'est une extension à la fois de la logique linéaire commutative et de la logique linéaire cyclique de Girard et Yetter (qui est elle-même une extension conservatrice classique du calcul de Lambek, introduit en 1958). Initialement, Paul Ruet a défini cette logique pour la programmation concurrente par contraintes, mais les applications potentielles en sont nombreuses. Dans NL il y a deux connecteurs autres que ceux de la logique linéaire, qui sont non commutatifs ; de nouvelles règles permettent de lier les structures commutatives et non-commutatives. Il existe deux présentations du calcul des séquents de NL, l’une utilisant des ordres partiels (en pratique des ordres série-parallèles), l’autre des variétés d'ordre série-parallèles. Nous avons choisi les séquents avec ordres partiels pour étendre la notion de "focusing" d'Andreoli et concevoir un prouveur de théorèmes. La construction théorique du langage est achevée [Rémi Baudot, présentation courte LICS’2000, WFLP’2002].

A côté de ces travaux qui visent à étendre l'expressivité du langage, nous avons cherché à intégrer à la programmation logique la modularité. Nous nous sommes restreints dans un premier temps au fragment multiplicatif de la logique linéaire. La modularité est obtenue en n'effectuant pas explicitement les résolutions, alors qu'en programmation logique classique la sélection de clause est conditionnée par le résultat des résolutions précédentes. L'applicabilité d'une clause résulte alors de la satisfaction d'un critère de correction globale. Nous avons analysé dans quelle mesure ce critère peut ne porter que sur l'interface, i.e. le résolvant, en interprétant la programmation logique en termes de composition de modules.

Prospectives

Nos travaux nous mènent naturellement à étudier les applications en Intelligence Artificielle ou en programmation distribuée. Il s'agira d'abord d'étendre la deuxième approche en intégrant la non-commutativité, de définir et implanter un langage de programmation, enfin de montrer dans quelle mesure cette approche est adaptée aux cas classiques.

Planification et logique linéaire

Dans des travaux antérieurs, nous avons utilisé le fragment multiplicatif de la logique linéaire pour formaliser de manière complète et correcte une suite d’actions. Une suite d'actions est représentée par une preuve dans une théorie de la logique linéaire dont les axiomes sont des séquents de Horn utilisant les connecteurs “fois“ et “plus“ dans le cas d'actions non déterministes, et seulement le connecteur “fois“ dans le cas d'actions déterministes.

Nous avons étudié le problème de la complexité de la recherche de preuve dans de telles théories : il est connu que la logique propositionnelle linéaire de Horn est indécidable dans le cas général (cas des connecteurs “fois“ et “plus“) et a la complexité du problème d'accessibilité dans les réseaux de Petri (cas du connecteur “fois“). Pour restreindre la complexité, nous avons utilisé (dans des travaux en collaboration avec Max Kanovitch, université de Moscou) des axiomes tels que le nombre de prédicats apparaissant dans la partie gauche est supérieur ou égal à celui apparaissant dans la partie droite. Cette condition, réalisée dans la formalisation des problèmes de planification usuels, permet de ramener la complexité à EXPTIME (temps exponentiel) dans le cas d'actions non déterministes, et à PSPACE (espace polynomial) dans le cas d'actions déterministes [Kanovitch & Vauzeilles, Mathematical Structures in Computer Science]

Nous nous sommes ensuite intéressés aux problèmes de planification comprenant un nombre non borné d’objets fonctionnels identiques. L’utilisation de la logique linéaire permet, dans ce cas, de restreindre de façon drastique l’espace de recherche puisqu’on obtient un espace polynomial au lieu d’exponentiel, dans le cadre d’actions non-déterministes [Kanovitch & Vauzeilles, CSL’03 & KGC]

Prospectives :

Nous cherchons à caractériser d'autres classes de problèmes de planification, dont la complexité pourrait être restreinte. D’autre part, nous comparons nos résultats à ceux obtenus en planification sans l’utilisation de la logique linéaire.

Logique linéaire, complexité et typage

La logique linéaire (LL) permet d'exprimer un contrôle fin de l'usage des ressources grâce aux modalités qui précisent leur duplication. Des variantes de la logique linéaire caractérisant certaines classes de complexité ont été proposées. Pour la classe PTIME (temps polynomial) nous avons étudié les logiques linéaires light et soft (respectivement dues à Girard et Lafont). Elles offrent une élimination des coupures polynomiale et sont PTIME-complètes. Vues comme des systèmes de types pour le lambda-calcul ou certaines de ses variantes elles assurent la propriété suivante: si un programme est bien typé alors on dispose d'une borne polynomiale en temps pour son exécution sur toute entrée. Deux démarches sont alors possibles :

- soit programmer dans un langage correspondant par l'isomorphisme de Curry-Howard au système logique;

- soit conserver le lambda-calcul standard et utiliser le système logique pour une analyse statique par typage.

Dans la perspective d'une automatisation du typage (à la manière du langage CAML par exemple) nous avons montré que pour le lambda-calcul l'inférence de type en logique light était décidable. Ceci est obtenu par une analyse structurelle du programme suivie de la résolution d'un système de contraintes [P. Baillot, IFIP TCS 2002 et réunion d'Action Spécifique Formal Methods for Mobility, décembre 2002].

Pour la logique soft nous avons adopté l'autre démarche. Nous avons défini une variante du lambda-calcul lui correspondant et entamé l'étude de la représentation des données et d'algorithmes dans ce langage. Pour cela nous avons étendu le système avec des types récursifs en gardant les mêmes propriétés [P. Baillot, M. Masseron, V. Mogbil, workshop Formal Methods for Mobility 2003].

Prospectives:

Nous souhaitons poursuivre l'étude de l'inférence de type en logique light ainsi que de la programmation en lambda-calcul soft et comparer l'expressivité concrète de ces langages à d'autres systèmes proposés dans la littérature pour garantir des bornes de complexité en temps et espace (Bellantoni-Cook, Hofmann). Ces recherches seront menées en particulier dans le cadre des ACI GEOCAL et CRISS.

Systèmes explicatifs : formalisation en Logique non commutative

A l'aide de la Logique non-commutative, nous avons formalisé un système de reconnaissance de l'écriture manuelle cursive.

Pour la reconnaissance de caractères, nous avons pu justifier de manière rigoureuse tous les choix de configuration effectués, tels que la normalisation des données, (toutes les données ont la même taille), et sous ces hypothèses, montrer que notre méthode est de complexité quasi-linéaire.

Pour la reconnaissance de mots par extension des règles du calcul défini, nous avons également montré que la complexité du problème dans ce cas devient explosive ; ce problème est équivalent en complexité au problème de marquage dans les Réseaux de Petri (de type exponentiel).[J. Castaing, International Conference in Artificial Intelligence and Symbolic Computing 2002].

Prospectives 

Dans l'immédiat, trouver des stratégies pour limiter en complexité la reconnaissance des mots. Et dans les deux ans à venir, écrire un prouveur de théorèmes "linéaire" pour la reconnaissance universelle : image - musique - video.

Logique et concurrence

Plusieurs approches visent à modéliser les situations de calculs concurrents, où plusieurs processus agissent en parallèle. Une première est celle des calculs de processus qui s'est développée par analogie avec le lambda-calcul : dans les calculs de base les processus ne peuvent que se synchroniser (comme dans CCS par exemple), alors que les versions les plus expressives comme le pi-calcul permettent le passage de noms. Nous avons, dans cet esprit, donné une sémantique opérationnelle au langage Claim. Ce langage de programmation permet la modélisation de systèmes multi-agents en intégrant à un calcul de processus avec mobilité une gestion des buts et des connaissances. Ces travaux sont effectués dans le cadre d'un projet LAFMI (Laboratoire franco-mexicain d'Informatique): Conception et développement d'un langage de programmation orienté-agent.

Une deuxième approche est issue de la programmation logique : la spécification du système est donnée par une formule, par exemple en logique linéaire, et le calcul procède par une recherche de preuve. De ce point de vue, nous cherchons à utiliser la programmation logique comme langage de spécification. Dans le même temps, nous essayons de caractériser logiquement la notion de concurrence stricte (développement d’un calcul des séquents et sémantique de ce calcul). Ce type de calcul est à rapprocher du calcul BI (calcul de pointeurs avec gestion des ressources).

Thème : Spécifications de systèmes et aide à la modélisation (Faouzi Boufarès, Christine Choppy, Gérard Garcia, Martin Heriberto Cruz Rosales, Sana Hamdoun, Kazem Lellahi, Laure Petrucci).

Dans ce thème, les différents aspects de la spécification et de la modélisation étudiés trouvent leurs applications notamment sur les systèmes dynamiques, concurrents et distribués, et les bases de données.

Pour les systèmes réactifs, la prise en compte et la combinaison adéquate des aspects données, contrôle, est essentielle. La notion d’état pour de tels systèmes est nécessaire mais complexe et la rendre implicite permet de satisfaire pouvoir d’expression et lisibilité.

Pour les bases de données, la formalisation des concepts et la notion d’état jouent un rôle important dans la modélisation des données et objets. La formalisation permet de mieux cerner l’intégration des bases de données et des langages de programmation et rendre l’état implicite permet un traitement algébrique et l’application des techniques de spécification.

Au niveau conceptuel la formalisation permet l’intégration des contraintes et l’application des techniques d’optimisation (collaboration avec l’équipe OCAD).

Spécification et Méthodologie

Différents aspects de la mise en œuvre des spécifications formelles sont explorés en établissant un lien avec des méthodes et langages utilisés dans l’industrie, tels que la notation UML, les schémas de problème (ou “ problem frames ” de M. Jackson), les “ patterns ”, etc.

Par ailleurs, pour pouvoir prendre en compte différents aspects (données, contrôle, composition de sous-systèmes, …) dans la spécification de systèmes réactifs, une extension de langages de spécification existants, tels que le langage CASL (Common Algebraic Specification Language) développé dans le cadre du projet CoFI (Common Framework Initiative) a été proposée : le langage CASL-LTL permet d’exprimer des propriétés dynamiques, les transitions entre états sont étiquetées par des ensembles d’événements, et les propriétés sont exprimées par des formules où peuvent figurer des opérateurs de logique temporelle. Une note sur ce langage a été écrite, puis modifiée pour tenir compte des remarques des membres du projet. Dans le cadre du groupe “Reactive“ du projet CoFI, les liens avec le langage UML sont étudiés pour faciliter l'utilisation des spécifications en liaison avec UML [C. Choppy & al., FASE 2000].

Une formalisation des schémas de problème (“problem frames“ de M. Jackson) exprimée en langage CASL et dans son extension CASL-LTL a été écrite ; pour chaque schéma étudié, “Translation frame“, “Information System frame“, “Control frame“, cette formalisation est accompagnée d’une méthode pour compléter la spécification engendrée, d’un cadre de vérification d’adéquation entre la conception résultante et les besoins exprimés, et d’une étude de cas détaillée où est illustrée l’application de ces idées [Choppy & al., « Recent Trends in Algebraic Development Techniques », 2000]. Ce travail a été poursuivi pour explorer les critères de choix d’un schéma de problème, et l’association dans la poursuite du développement avec les choix de styles d’architecture [C. Choppy & al., chapitre de « Recent Trends in Algebraic Development Techniques », 2003].

Les deux aspects, données et contrôle, sont présents dans les formalismes “mixtes“ qui peuvent être bien adaptés pour les systèmes réactifs. Pour développer une spécification dans ce cadre, il s'agit d'exprimer les aspects relatifs aux activités concurrentes, aux composants séquentiels, et aux données manipulées. Les fonctionnalités “externes“ du système permettent d'identifier les services que les processus doivent rendre. Pour chaque processus, on peut envisager différents modes de composition parallèle de ses fonctionnalités indépendantes. On étudie pour chaque fonctionnalité, les conditions éventuelles sous lesquelles elle peut avoir lieu et les communications associées à cette activité : ces éléments sont utilisés d'une part pour la construction de l'automate décrivant le fonctionnement du processus, d'autre part pour la spécification du type de données associé au processus. On procède ensuite par étapes : les informations associées aux transitions de l'automate fournissent d'autres éléments exploités pour la partie donnée. A chaque étape, on peut identifier les éléments résultant de “ l'analyse ” du spécifieur, et l'exploitation automatisée qui peut en être faite pour faciliter les étapes ultérieures et fournir tout ou partie des résultats attendus. On combine ainsi, avec méthode, l'utilisation d'outils automatiques, et le résultat du raisonnement humain [C. Choppy & al., AMAST’2000 (International Conference on Algebraic Methodology and Software Technology), APSEC’2001 (Asia-Pacific Software Engineering Conference), FASE’2001 (Fundamental Approaches to Software Engineering) et INT’2000 (Integration of Specification Techniques with Applications in Engineering)].

Un travail définissant une méthodologie plus générale de développement et de spécification de systèmes complexes a ensuite été développé (article soumis à une revue).

Dans le cadre de cette activité, il y a des collaborations avec Gianna Reggio, professeur à l’Université de Gênes (Italie), avec Maritta Heisel, professeur à l’Université de Magdebourg (Allemagne), avec Claude Le Tallec, ingénieur (ONERA), avec Pascal Poizat, maître de conférences à l’Université d’Evry (à la suite de sa thèse soutenue à Nantes), avec Jean-Claude Royer, maître de conférences à l’Université de Nantes.

Prospectives :

Partant des travaux réalisés sur la formalisation des problem frames, on pourra décrire une méthode générale de spécification qui permette de combiner des composants de caractéristiques répertoriées ; pour chacun de ces composants, proposer une méthode adaptée. L’applicabilité de ces idées est testée sur des études de cas de taille industrielle. Une présentation visuelle adaptée est proposée afin d’assurer une bonne lisibilité aux spécifications de problèmes de grande taille. On proposera également une expression en UML des schémas de problème afin de faciliter leur utilisation en pratique. On explorera également les extensions nécessaires pour la prise en compte du temps réel, par exemple en s’appuyant sur l’utilisation combinée d’automates temporisés. Enfin, une utilisation combinée des schémas de problème, des styles d’architecture (de logiciels), et des schémas de conception (“ design patterns ”) est proposée pour prendre en compte les différentes étapes du développement (spécification, conception, conception détaillée – proche de l’implémentation).

Modélisation des objets, spécification algébrique avec état

Le thème général des recherches dans cet axe a été la théorie des bases de données et plus particulièrement la modélisation des données et des objets.

Ces recherches, suite et extension de travaux antérieurs, ont été menées dans les directions suivantes liées les unes aux autres :

- La définition d’un modèle formel pour objets, influencé par des techniques venant de la théorie des catégories, incluant tous les aspects des objets : héritage, surcharge, valeurs nulles, différents modes d’évaluation, et le problème crucial du changement d’état,

- Les travaux sur les types de collections comme une application de la théorie des monades en bases de données, influencés par les travaux de P. Bunemann, V. Tannen et E. Moggi,

- Les travaux sur des spécifications algébriques avec état implicite (approche de Y. Gurevich),

- Les travaux influencés par la théorie des catégories et des esquisses, sur la formalisation des méthodes conceptuelles en bases de données ainsi que les contraintes de ces modèles, permettant de définir une méta-spécification dont les modèles (au sens des spécifications algébriques) sont les diagrammes Entité-Association généralisés.

La combinaison de ces travaux a permis de donner un modèle algébrique complet pour les données et objets, dans le contexte des bases de données. Ce modèle prend en compte tous les aspects statiques et comportementaux des objets. Ces travaux prouvent que ce modèle convient à toutes les étapes de modélisation, de la spécification à l’implantation. Ces techniques de formalisation sont appliquées aux langages objet, en particulier pour définir une sémantique algébrique des aspects séquentiels du langage Java.

Dans le cadre de ces activités, il y a des collaborations avec Alexandre Zamulin du Centre Sibérien de l’Académie des Sciences de Russie et avec Nicolas Spyratos de l’Universite Paris 12, LRI, Orsay.

Ces travaux ont donné lieu à plusieurs publications internationales [K. Lellahi & al., « Perspective of System Informatics » (PSI) 2001, Advances in Database and Information System (ADBIES) 2001, Computer Science and Information Technologies (CSIT) 2001, Formal Techniques for Java Programs (FTFJP) 2002 et FTFJP 2003], une contribution à des livres [Theoretical Aspects of Computer Science, advanced lectures, LNCS No 2292 paru en 2002], et la soutenance d’une Habilitation à Diriger des Recherches [HDR de K. Lellahi soutenue le 20.12.01].

Prospectives

Dans les travaux à venir, ces techniques de formalisation seront appliquées aux aspects concurrents du langage Java et aux mises à jour d’état à partir d’une vue, en particulier pour ses applications aux bases de données et aux entrepôts des données.

Compilation et Optimisation de Schémas conceptuels de Bases de Données

L’objectif de cet axe est l’analyse et le développement d’un outil d’aide à la modélisation de Bases de Données et plus spécialement dans un environnement distribué, prenant en compte les divers types de contraintes.

Plusieurs catégories de contraintes ont été présentées dans la littérature. Les plus connues dans la modélisation de bases de données sont les contraintes de cardinalités et les notions de clés et de dépendances fonctionnelles.

Alors que les propriétés formelles de chacune de ces catégories sont largement maîtrisées, peu de travaux et d'outils d'aide à la conception sont faits pour intégrer tous ces concepts à la fois. Les outils d'aide à la conception, basés sur l’approche UML ou le modèle Entité-Association (EA) et ses extensions, qui existent aujourd'hui n'offrent pas la possibilité de contrôler la cohérence globale des différents types de contraintes. Les conflits qui peuvent exister entre d'une part les contraintes de cardinalités elles-mêmes et d'autre part entre les contraintes de cardinalités et d’autres types de contraintes tels que les dépendances fonctionnelles par exemple, ne sont pas détectés.

Le but de ce travail est multiple :

- Modéliser les différents types de contraintes d’un schéma conceptuel de Bases de Données,

- Vérifier la cohérence de tels systèmes en utilisant les techniques de satisfaction de contraintes (Techniques de programmation en nombres entiers),

• Présenter un outil d'analyse de schémas conceptuels de bases de données et plus spécialement dans un environnement distribué,

• Etablir une passerelle conceptuelle entre les deux approches UML et EA étendu, [F. Boufarès, International Conference on Concurrent Engineering, 2003].

• Modélisation et construction d’entrepôts de données hétérogènes.

Thème : Combinatoire algébrique (Christophe Tollu, Frédéric Toumazet)

Ce thème correspond à la création en 2001 par le Département des Sciences et Technologies de l'Information et de la Communication, de la JemSTIC (Jeunes chercheurs, Jeunes équipes, Mobilité) "Outils combinatoires pour le développement et l'analyse d'algorithmes en physique mathématique" portée par Frédéric Toumazet.

Depuis 2000, nous nous sommes consacrés à l’étude de divers problèmes combinatoires soulevés en théorie des représentations des algèbres intervenant en physique (algèbres de Weyl et de Heisenberg, algèbres du groupe unitaire et du groupe symétrique). Ces problèmes se réduisent souvent au calcul de multiplicités lors de la décomposition en modules simples ou irréductibles de produits tensoriels.

Les représentations (irréductibles) du groupe symétrique sont intimement liées à des nombres connus sous le nom de coefficients de Littlewood-Richardson, dont l'importance est attestée par les contextes nombreux et variés dans lesquels ils apparaissent. Ces nombres sont paramétrés par trois partitions et peuvent être définis de manière purement combinatoire. Dans le prolongement des récentes et spectaculaires avancées dues à Knutson, Tao et Woodward (résolution de la conjecture de saturation et de la conjecture de Fulton), nous avons étudié les relations entre ces nombres et leur dilatation (chaque part est multipliée par l'entier N > 0). Nous avons accumulé assez de données expérimentales pour conjecturer, premièrement que pour des parts fixées, la dilatation est un polynôme en N de coefficient constant égal à un, deuxièmement que les coefficients du numérateur de la série génératrice (rationnelle réduite) de ces nombres sont positifs. En adaptant le modèle combinatoire des ruches dû à Knudson et Tao aux nombres de Kostka, nous avons conjecturé le même comportement pour les dilatations de ces derniers nombres. Nous avons démontré ces trois conjectures dans les cas restreints où toutes les partitions intervenant dans les calculs ont au plus quatre parts ou encore lorsque l’une des partitions est du type escalier. La polynomialité des coefficients dilatés de Kostka et Littlewood-Richardson a par ailleurs été démontrée par Derksen et Weyman et par Billey, Guillemin et Rassart.

Parallèlement, nous avons commencé de travailler avec Gérard Duchamp (Rouen) sur des réalisations de l'algèbre de Weyl déformée W_q. Cette algèbre joue un rôle de premier plan en physique mathématique, car les relations de commutation qui la définissent expriment une forme d'interpolation entre des statistiques fermioniques et bosoniques. En construisant l'espace de Fock associé, Don Zagier a donné une condition sur la déformation q, suffisante pour qu'il existe une réalisation de W_q. Nous avons construit une réalisation explicite de la q-algèbre de Weyl (dans un cas particulier) dans laquelle les opérateurs sont définis de façon purement combinatoire, à l'aide d'outils développés pour la théorie des fonctions symétriques non commutatives (produit de battage déformé et dérivée non commutative).

Enfin, Frédéric Toumazet a collaboré, avec Ronald C. King (Southampton, Royaume-Uni), et Brian G. Wybourne (Torun, Pologne), à un travail de généralisation au q-Vandermonde de propriétés connues dans le cas du déterminant de Vandermonde classique, obtenu comme somme de fonctions symétriques (fonctions de Schur) dont les multiplicités sont des entiers. Ces propriétés sont une extension « quantique » de propriétés découvertes pour le cas classique (les coefficients sont alors remplacés par des polynômes en q) et notamment elles ouvrent des possibilités algorithmiques pour le calcul des puissances de ces déterminants (calculs explicites obtenus pour le carré jusqu’à l’ordre 9), qui fait appel à la règle de Littlewood-Richardson.

Prospectives

Nous prolongerons notre étude de problèmes combinatoires associés aux représentations. Premièrement, au travers de l’étude des polynômes intervenant dans le calcul des puissances du q-Vandermonde, cherchant à mettre en évidence des régularités dans leur forme et leur spécialisation pour différentes valeurs de q (on retrouve les coefficients « classiques » pour q=1). Deuxièmement nous étudierons une généralisation, proposée par Foda, Leclerc, Okado et Thibon en 1998, des coefficients de Littlewood-Richardson, qui se spécialise à la fois en des polynômes définis à l'aide de tableaux de rubans, et en les constantes structurelles d'algèbres de fusion des théories conformes de champs de Wess-Zumino-Witten associée à SU(n). Notre objectif est de reprendre, pour le généraliser aux coefficients de Foda et alii, l'algorithme de Kac et Walton, calculant les coefficients restreints, et de trouver pour ces derniers des interprétations combinatoires. Enfin, les travaux sur l’algèbre de Weyl déformée font apparaître une combinatoire riche, en particulier au travers des opérateurs de réordonnancement. Leur étude nécessite d’établir des liens précis entre transformations de suites et algèbres de substitutions.

Tous ces travaux renforceront les collaborations existantes avec le Phalanstère de Combinatoire de Marne-la-Vallée, l'Institut de Physique de Torun (Pologne), et l'université de Southampton (Royaume-Uni).

Thème : De la représentation et du raisonnement temporel à Henri-Auguste Delannoy (Sylviane Schwer)

Le formalisme des S-langages, qui permet d'une part d'unifier les représentations des objets "dits" temporels (points, intervalles, chaînes de points et/ou intervalles) et de leurs relations qualitatives, et d'autre part de faire un raisonnement fondé sur les opérateurs S-classiques des langages formels (c'est-à-dire sans tableau de transitivité ni systèmes d'inférence et en traitant les relations quelles que soient leurs arités) a été parachevé. A partir du formalisme des S-langages, une représentation graphique des relations entre n objets sous forme de chemins dans le treillis d'entiers de dimension n s'est imposée. Ainsi, en dimension 2, l'ensemble des relations est en bijection avec les chemins de Delannoy et est nombré par les nombres de Delannoy.

En collaboration avec J.-M. Autebert et M. Latapy (Université Paris 7), un système de réécriture, appelé de Delannoy a été mis en évidence. Ce système permet de traduire la notion intuitive de voisinage développée par Freksa, de générer l'ensemble des relations binaires entre deux objets à partir d'une relation particulière et munit l'ensemble d'une structure de treillis distributif. En collaboration avec J.-M. Autebert, le résultat a été généralisé au cas n-aire et la structure obtenue est un treillis non modulaire.

Le dénombrement des ensembles de relations qualitatives entre n objets, obtenu facilement grâce au formalisme des S-langages, généralisant le cas binaire déjà étudié indépendamment par G. Ligozat et L. Al-Khatib, a conduit à rechercher des structures similaires dans différents domaines mathématico-informatiques et à mettre en évidence la partie temporelle traitée, à savoir la notion d'instant - au sens de Russell - et celle de chronologie abstraite. C'est par l'étude des marqueurs temporels dans le domaine de la linguistique qu’on pense obtenir de nouveaux résultats en représentation et raisonnement temporel, cela en collaboration avec l'équipe Lalicc de l'Université Paris IV.

Prospectives

Un travail pluridisciplinaire autour de Delannoy avec le REHSEIS(UMR 7596), le LaLICC(UMR 8139) et une partie de l'équipe OCAD et les mathématiques a été proposé dans le cadre de l'action concertée histoire des savoirs. Il s'agit de l'étude de la communauté française des combinatoriciens et théoriciens des nombres dans l'entre-deux guerres (1870-1914) et de la répercussion de leurs travaux de nos jours.

Les recherches sur le temps en linguistique vont se poursuivre, notamment avec une collaboration accrue avec le LaLICC.

Thème : Analyse linguistique de documents du web (Christophe Fouqueré, collaboration avec le LLI, projet France-Québec).

(cf thème Analyse linguistique équipe RCLN)