%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\subsection{Thèmes de recherche} La logique linéaire (LL), 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. %Nos travaux portent sur l'étude ou l'utilisation de la logique linéaire % (ou de ses dérivées : raffinements, extensions, ...) en vue d'applications % en informatique. Nos travaux portent sur l'utilisation de la LL dans les deux principaux paradigmes de calcul logique: la \textit{correspondance preuves-programmes} d'une part, avec ses applications à la programmation fonctionnelle; le calcul par \textit{recherche de preuve}, ou \textit{programmation logique}, d'autre part. Dans le premier cas une preuve formelle peut être vue comme une dérivation de type d'un programme; dans le second elle correspond à l'exécution de celui-ci. La LL a permis la définition d'outils puissants pour ces deux approches, comme les \textit{réseaux de preuves}, une représentation des démonstrations sous forme de graphes. Elle permet aussi de distinguer plusieurs familles de connecteurs logiques: \textit{additifs}, \textit{multiplicatifs} et \textit{exponentiels}, avec des comportements spécifiques en termes d'usage des ressources. %Dans ce contexte, trois cadres applicatifs ont particulièrement été étudiées % dans le cadre de l'\acs{ACI} \textsc{geocal} (2003-06) : Dans le contexte des deux paradigmes de programmation mentionnés, trois domaines applicatifs ont été particulièrement étudiés dans le cadre de l'\acs{ACI} \textsc{geocal} (2003-06) : %la LL comme système % de types par application à l'étude de la complexité implicite des programmes %où les systèmes de types permettent de garantir une borne temporelle, la LL comme système de types permettant de garantir des bornes de complexité sur les programmes;les structures de preuves comme solution de problèmes de planification d'Intelligence Artificielle; la LL comme base de la programmation logique où les clauses sont définies comme réseaux de preuve partiels. Nous avons aussi débuté un projet de spécification et développement d'un langage de programmation adaptée pour le web. Un site web est vu comme composé de parties à contenu évolutif à typage statique, permettant ainsi au programmeur de concevoir des sites Web hautement interactifs proposant une plus grande souplesse et simplicité, ainsi qu'une plus grande fiabilité. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{Logique linéaire et complexité implicite} \textbf{Contexte.} L'analyse logique de la réutilisation de ressources dans la LL a permis de définir des variantes de ce système correspondant à différentes classes de complexité calculatoire: les LL Light (LLL, Girard 1995) et Soft (SLL, Lafont 2002) pour le temps polynomial (Ptime) et ELL pour le temps élémentaire. Ces travaux s'inscrivent dans le domaine de la Complexité Implicite, qui vise à definir des calculs ou des langages où tous les programmes ont par construction une borne de complexité donnée (par exemple Ptime). \textbf{Objectifs.} Nous cherchons par le biais de la Logique linéaire et de la Complexité implicite à mieux comprendre le calcul à ressources bornées, et en particulier en temps polynomial. D'une part nous souhaitons en dériver des méthodes pour vérifier statiquement des bornes de complexité sur les programmes fonctionnels. Il est en particulier nécessaire de déterminer l'efficacité de ces méthodes et leur couverture en termes d'expressivité intensionnelle (algorithmique). D'autre part, plus fondamentalement nous étudions par ce biais les classes de complexité de problèmes (notamment grâce aux circuits booléens) et la sémantique des programmes à complexité bornée. \begin{itemize} \item \textbf{Typage et garantie de complexité en lambda-calcul:} Nous avons poursuivi l'étude de l'utilisation des logiques LLL et ELL comme systèmes de types pour le lambda-calcul, garantissant respectivement des bornes polynomiales et élémentaires sur l'exécution des programmes (via les réseaux de preuves). Nous avons ainsi montré que l'inférence de type en LLL pour le lambda-calcul était décidable \cite{B04b}. En collaboration avec Terui (NII, Tokyo) nous avons ensuite défini un sous-sytème de cette logique, appelé DLAL, offrant de meilleures propriétés vis-à-vis du lambda-calcul: les programmes typés sont en effet Ptime pour la réduction du lambda-calcul, et non seulement pour la réduction des réseaux \cite{BT04}. Par ailleurs nous avons donné des algorithmes d'inférence de type efficaces (Ptime) dans ELL et DLAL pour le lambda-calcul \cite{BT05,ABT05,ABT07}. Enfin, nous avons analysé la \textit{réduction optimale} (au sens des travaux de Lévy, Lamping) des programmes du lambda calcul typé dans LLL (et ELL, DLAL \dots). Celle-ci définit des stratégies d'exécution des programmes minimisant en un certain sens le travail d'évaluation et décrites par des règles de réécriture de graphes. Nous avons démontré que pour le lambda-calcul typé dans LLL, la réduction optimale est de complexité en temps polynomiale \cite{BaillotCoppolaDalLago07}. Ce résultat a été obtenu en utilisant des outils de \textit{géométrie de l'interaction} venant des réseaux de preuves. \item \textbf{Complexité implicite et expressivité:} Comme les systèmes LLL et SLL permettent de représenter toutes les \textit{fonctions} Ptime mais pas tous les \textit{algorithmes}, il est intéressant, d'un point de vue pratique en particulier, de considérer des extensions de ces logiques. Nous avons ainsi étudié l'extension de SLL avec des types récursifs et défini un lambda-calcul étendu spécifique pour ce langage (\cite{BM04}). D'autre part avec Dal Lago (Bologne) nous avons montré que LLL sans second-ordre mais avec types récursifs était complet pour la classe Ptime \cite{DLB06}. Par ailleurs nous nous sommes intéressés au modèle de Blum-Shub-Smale (BSS) qui permet de représenter le calcul sur les réels ous sur d'autres anneaux. Nous avons donné une nouvelle mesure d'espace dans ce modèle, permettant de définir des classes LOGSPACE et PSPACE (\cite{deNaurois06}). Avec Pedicini (Rome) nous avons montré qu'une extension du lambda-calcul typé dans LLL permettait de caractériser la classe BSS Ptime sur un anneau arbitraire \cite{BP04}. Nous avons aussi considéré une autre approche de la complexité implicite, basée sur les systèmes de réécriture, les \textit{quasi-interprétations} de Bonfante-Marion-Moyen, et étudié son expressivité algorithmique en donnant des conditions nécessaires sur les algorithmes admettant des quasi-interprétations \cite{BDLM06}. Enfin, nous avons introduit la notion de \textit{graphe de contrôle de re ssources} comme un cadre général permettant de regrouper différentes analyses d e terminaison de programme et de complexité. \item \textbf{Complexité et réseaux de preuves:} Initiée par Terui et Mairson (2003-04), une autre approche logique de la complexité consiste à représenter une fonction non pas par une seule preuve (comme dans LLL) mais par une famille uniforme de preuves, où chacune correspond à une taille de données fixée, à la manière des circuits booléens. Ces derniers sont un modèle de calcul parallèle usuel en théorie de la complexité. Dans cette perspective, il est suffisant de considérer un petit fragment de la LL, sans duplication : la logique linéaire multiplicative (MLL). En passant à la syntaxe des réseaux de preuves qui est intrinsèquement parallèle, Terui a donné une traduction des circuits booléens dans les réseaux de preuves et vice-versa. En y ajoutant une notion d'uniformité pour les réseaux de preuves préservée par cette approche nouvelle, nous caractérisons dans les réseaux de preuves, la classe de complexité NC : ce sont les fonctions effectivement parallélisables \cite{MR07}. Nous avons aussi étendu l'approche initiale à d'autres familles de circuits et à d'autres fragments usuels de la LL préservant l'accélération due au parallélisme du modèle de calcul. Notamment la classe de circuits NNC, ajoutant du non déterminisme à NC, est montrée équivalente à la classe de réseaux de preuves booléens de la logique linéaire multiplicative et additive (MALL). Nous caractérisons ainsi la classe NP usuelle dans les réseaux de preuves MALL \cite{MR07}. \item \textbf{Sémantique en complexité implicite:} Enfin, nous étudions les invariants dénotationnels des logiques linéaires à complexité implicite afin d'éclairer leur structure mathématique. À cette fin, nous avons introduit les espaces cohérents stratifiés \cite{B04a} et nous considérons actuellement les contraintes capturant la complexité implicite au sein de sémantiques de la logique linéaire. \end{itemize} Ces travaux ont été menés dans le cadre de l'\acs{ACI} \textsc{criss} (2003-06) et depuis décembre 2005 du projet No-Cost (projet \acs{ANR} Jeunes chercheuses et jeunes chercheurs). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{Logique linéaire et planification} Dans plusieurs articles pr\'ec\'edents nous avons montr\'e que la logique lin\'eaire permettait de mod\'eliser de façon ad\'equate le probl\`eme typique d'Intelligence Artificielle de r\'ealiser un plan d'actions \`a accomplir par un robot pour atteindre un \'etat final, en partant d'un \'etat initial donn\'e. A cette fin, nous avons introduit la logique lin\'aire de Horn et montr\'e que contrairement \`a l'ind\'ecidabilit\'e de la logique lin\'eaire propositionnelle de Horn, le probl\`eme de planification est d\'ecidable pour une large classe de syst\`emes de robots. Nous avons en particulier prouv\'e que le probl\`eme de planification \'etait EXPTIME-complet pour les syst\`emes de robots permettant des actions non d\'eterministes et que cette complexit\'e pouvait \^etre r\'eduite \`a PSPACE pour les syst\`emes de robots dont les actions sont uniquement d\'eterministes. \medskip Au cours de la p\'eriode 2003-2006, nous avons poursuivi cette \'etude de la planification dans deux directions : \begin{itemize} \item {\em La planification concernant des domaines contenant un grand nombre d'objets identiques.} Nous avons montr\'e que dans ce cas, la logique lin\'eaire permettait une r\'eduction drastique de l'espace de recherche (polynomial au lieu d'exponentiel). Pour cela, nous remplaçons le nombre non born\'e de noms sp\'ecifiques d'objets par un nom g\'en\'erique et nous contractons ainsi l'espace de recherche exponentiel sur les objets `r\'eels' en un espace de recherche polynomial sur un objet `g\'en\'erique' en exhibant une formulation plus abstraite et en prouvant que la solution peut \^etre traduite directement en des solutions polynomiales (et optimales) du probl\`eme initial \cite{DBLP:conf/csl/KanovichV03, KanVau-TCS}. \item {\em La planification temporelle.} L'hypoth\`ese faite dans les pr\'ec\'edents travaux \'etait que les effets des actions \'etaient instantan\'es. Dans ce cadre, les plans et les strat\'egies associ\'ees sont finies, si on suppose qu'il n'y a qu'un nombre fini d'\'etats. Nous avons ensuite \'etudi\'e la planification pour des actions avec effets diff\'er\'es : m\^eme dans le cas d'un nombre fini d'\'etats, la difficult\'e rencontr\'ee est qu'alors les strat\'egies sont de branchement infini car le nombre de d\'elais possibles est infini, puisque le temps est suppos\'e \^etre le temps r\'eel. Nous avons montr\'e que, m\^eme dans ce cadre plus complexe, la correspondance entre les preuves en Logique Linéaire et les plans était maintenue \cite{KanVau-FSTTCS}. \end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{Programmation par modules} La programmation logique a connu de nouveaux développements depuis quinze ans, tant dans la compréhension profonde du mécanisme de calcul par le biais de l'étude de la normalisation des preuves, que dans l'intégration de la concurrence dans le calcul par une formalisation en théorie des graphes. Ainsi, Andreoli a pu montré que les propriétés d'associativité et de commutativité des connecteurs alliées à la propriété de \textit{focalisation} induisent une polarisation des formules, une stratification des formules, des réseaux de preuves (cette notion fondamentale est également considérée dans les travaux de Girard sur la ludique ou de Laurent sur la logique linéaire polarisée). Le fait de pouvoir normaliser les preuves par {\it polarisation} en LL permet de considérer celle-ci comme un langage de programmation (la décomposition d'une formule polarisée correspond à l'application d'une clause en programmation en logique classique). En notant que la présentation par réseaux de preuves de la LL est une déséquentialisation de celles-ci, il est possible de rendre concurrente la programmation sous réserve de vérification d'un critère de correction garantissant la validité. En d'autres termes, la programmation logique usuelle est basée sur une réduction étape-par-étape de buts à prouver au moyen d'une résolution ou d'une règle de progression, la correction d'un calcul est alors réduite à un appariement entre une certaine partie du but courant et la tête d'une clause choisie (appariement structurel dans le cas où la LL complète est considérée). A contrario, l'approche par réseaux de preuves initiée par Andreoli est un cadre naturel de modélisation de la programmation concurrente. Nous avons étudié cette approche d'abord dans le cadre simple multiplicatif puis dans un cadre avec exponentiels en adoptant un point de vue de théorie des graphes. Clauses de notre système, les {\it modules}, sont des réseaux de preuve partiels. Tenant compte du fait que la LL est polarisée, nos objets de base sont alors des structures de preuve avec deux strates, appelés {\it structures bipolaires} ou {\it modules élémentaires}. Un programme logique est alors donné par un ensemble de telles structures bipolaires et son exécution résulte de la composition de ces structures, moyennant la satisfaction d'un critère de correction. Dans le cadre multiplicatif, nous avons étudié les modules fermés. Un module fermé correspond à un calcul terminé. Cette étude jouet nou s a permis de préciser les mécanismes de correction que nous avons généralisés ensuite. Le mécanisme de correction que nous utilisons est une forme polarisée du critère de Danos-Regnier. Le critère de Danos-Regnier est basé sur les propriétés graphiques des réseaux de preuve : les structures de preuve correctes sont dans un certain sens connexes et acycliques. Nous en avons déduit un critère de correction par réécriture pour les modules fermés. Nous avons montré que ce critère peut être prolongé aux modules bipolaires ouverts (correspondant à des exécutions partielles de programmes logiques) en remplaçant le critère de connexité par un critère de {\it connectabilité}. Nous avons enfin étudié comment il était possible de vérifier incrémentalement ces critères\cite{cfvm05SD}. Nous avons récemment entrepris l'extension de cette étude au cas exponentiel, le cas le plus simple étant de considérer que les modules bipolaires sont simplement réutilisables. Enfin nous avons généralisé le langage de module au cas général (exponentiels autorisés dans les modules) en donnant le critère de correction correspondant\cite{cfvm06-TCS}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{Programmation et web} Les sites Web étaient il y a quelques années composés essentiellement de pages statiques, mais de plus en plus, ces pages sont générées automatiquement par le serveur en fonction des requêtes du client et du contenu de bases de données. Récemment est apparue une troisième génération de sites, proposant une interactivité encore plus grande en utilisant des modifications dynamiques calculées côté client (Javascript , AJAX). Les langages traditionnellement utilisés pour programmer un site Web, par exemple PHP, Zope ou JSP, ne sont pas vraiment adaptés à ces nouvelles exigences des développeurs Web. Même lorsque le comportement dynamique est limité au côté serveur, des sites complexes deviennent vite très difficiles à développer et maintenir dans ces langages. Nous pensons que les concepts issus de la recherche théorique sur les langages de programmation peuvent permettre de résoudre ces problèmes. Nous nous sommes fixés comme objectif de définir une façon radicalement nouvelle de programmer des sites Web hautement interactifs proposant une plus grande souplesse et simplicité pour le programmeur, ainsi qu'une plus grande fiabilité. Notre première idée consiste à se départir du modèle de programmation traditionnel des sites page après page pour considérer au contraire un site dans sa globalité et rapprocher sa conception de celle d'une application traditionnelle. Il faut cependant prendre en compte des spécificités telles que la possibilité de revenir en arrière dans l'exécution du programme (bouton « back » des navigateurs) ou d'avoir plusieurs fils d'exécution simultanés (duplication d'une fenêtre). Ce sont des problèmes difficiles, souvent mal résolus dans les sites actuels. Le concept de « continuation » utilisé en programmation fonctionnelle permet de résoudre ce problème de manière très élégante et puissante. Le typage nous permettra en outre d'avoir un contrôle précis des liens et formulaires garantissant l'absence de liens morts et l'adéquation entre un formulaire et la page cible. Enfin ce style de programmation nous permettra d'avoir une gestion totalement transparente des sessions, sans que le programmeur n'ait à se préoccuper du passage et de la récupération des paramètres de session à chaque page. Le typage nous permettra également de résoudre un point important qui fait défaut dans les outils actuels : la génération de pages conformes aux standards. Le Web repose sur des standards édictés par le W3C, qui garantissent l'interopérabilité et l'accès universel aux informations. Aujourd'hui il est impossible de garantir la validité d'une page générée dynamiquement puisque les outils de validation ne peuvent prendre en compte que des pages statiques. Nous proposons de nous appuyer sur des travaux théoriques sur le typage de documents XML, qui nous permettrons de garantir la validité des pages grâce à une analyse statique du programme. Cette étude se fait en coordination avec une entreprise italienne (Net7, Pise) spécialisée dans la conception de sites web avec laquelle un projet Marie Curie - Transfer of Knowledge a débuté en 2006, en collaboration avec une équipe de PPS (projet ANR jeune chercheur débutant fin 2006). Ce projet fait suite au projet HyperLearning (\url{http://www.hypernietsche.org}) intégrant des équipes en sciences humaines et en informatique pour lequel nous collaborons dans le cadre d'un \acs{GDRE}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsubsection{De la repr\'esentation et du Raisonnement Temporel} S. Schwer a montré que les relations temporelles qualitatives sont en correspondance naturelle avec une variante d'un probl\`eme d'analyse combinatoire standard~: celui des combinaisons.\ Une fa\c{c}on \'el\'egante de d\'ecrire ces objets est celle des mots \'ecrits sur un alphabet de second ordre, {\it i.e.}~ensemble de parties d'un alphabet de base.\ L'alphabet de base d\'ecrit les identit\'es des objets temporels manipul\'es, ses parties repr\'esentant des {\em types d'instants} au sens de points de synchronisation.\ C'est ainsi qu'\`a partir d'une repr\'esentation math\'ematique non temporelle, nous avons restitu\'e une certaine temporalit\'e \`a ce probl\`eme : la temporalit\'e \'ev\'enementielle.\ Cette repr\'esentation permet de se d\'egager du cadre binaire dans lequel les relations temporelles sont trait\'ees par les diff\'erentes logiques utilis\'ees, de d\'enombrer et d'\'enum\'erer les relations qualitatives temporelles $n$-aires, et de fournir une repr\'esentation spatiale de chacune de ces relations dans un espace de dimension $n$, c'est-à-dire le nombre d'éléments en relation et non en fonction de la taille des éléments à l'intérieur d'une relation binaire (comme le fait le modèle de Ligozat). De plus, cette spatialisation conserve un sens temporel, puisqu'elle associe à une chronologie, une promenade sans perdre aucune des propriétés mises en lumière par les modèles précédents.\ J.-M.\ Autebert et S. Schwer ont prouv\'e que l'ensemble de ces relations forme une classe d'\'equivalence d'un syst\`eme de r\'e\'ecriture et que cette classe, pour l'ordre induit par la d\'erivation, poss\`ede une structure de treillis distributif dans le cas binaire, non modu\-laire (donc non distributif) d\`es que $n\geq 3$. Dans le cadre d'un nouveau groupe de travail, en collaboration avec une spécialiste du permutoidre (treillis des permutations) et des groupes de Coxeter de l'EHESS (Claude Barbut), S. Schwer a continué, dans le cadre de sa délégation au Lallic, à étudier les propriétés des treillis associés aux S-langages. Ce travail d\'epasse largement le cadre temporel.\ Il a permis en parti\-culier de fournir une application non triviale des chemins de Delannoy, bien connus des sp\'ecialistes de parcours dans les treillis discrets et d'enrichir l'encyclop\'edie des s\'equences enti\`eres de Sloane d'une nouvelle suite et de plusieurs r\'ef\'erences directes aux articles de Delannoy. Les applications abondent, en particulier dans le domaine des s\'equences audiovisuelles, en bases de donn\'ees temporelles, dans les syst\`emes d\'ecisionnels, en planification, en diagnostic, dans l'\'etude des s\'equences g\'en\'etiques \ldots Le raisonnement temporel est une classe particuli\`ere de probl\`emes de sa tisfaction de contraintes.\ Il se traduit en termes d'op\'erations alg\'ebriques classiques sur les S-langages (intersection, shuffle).\ Un probl\`eme de satisfaction de contraintes temporelles qualitatives admet une solution si et seulement si le langage temporel associ\'e est non vide.\ Chacune de ces solutions est donn\'ee par un mot qui est intrins\`equement une chronologie. Les calculs sont de type fortement paresseux afin de juguler, autant que faire se peut, l'explosion combinatoire inh\'erente \`a ce genre de probl\`eme.\ Nous avons montr\'e, en particulier, que dans le cas de contraintes ``convexes'', nous avons la m\^eme complexit\'e de calcul que par celui des r\'eseaux. Si le formalisme des S-mots permet de repr\'esenter les mod\`eles temporels discrets comme ceux de Allen, Ladkin, Ligozat ou des modèles linguistiques ponctuels (de Bauz\'ee\-/Reichenbach, de Marc Wilmet et Co Vet), intervallaires (de Moeschler et Laurent Gosselin), ... nous nous proposons de l'appliquer dans le cadre des interactions géniques. Une S-lettre est un état du cycle de vie dans le développement d'un organisme. Cette représentation permettra de reconstituer le réseau d'interaction. \subsubsection{Histoire des Sciences : Henri-Auguste Delannoy} S. Schwer s'est attachée depuis quelques années à l'étude de l'oeuvre de Delannoy\cite{AutebertSchwer03a}.\ Alors que nous connaissons les personnes associ\'ees aux suites portant leur nom, comme Eug\`ene Catalan (1814--1894), Axel Thue (1863--1922), Ernst Schr\"oder (1841--1902), Walther von Dyck (1856--1934), Jan {\L}ukasiewicz (1878--1956), Eric Temple Bell (1883--1960) ou bien Theodore Motzkin (1908--1970), aucun article de ces trente derni\`eres ann\'ees ne cite un article de cet auteur.\ Les seules r\'ef\'erences renvoient soit au livre de combinatoire de Louis Comtet soit \`a un article de Errera, qui eux m\^emes renvoient au livre de th\'eorie des nombres de Lucas. C'est \`a partir de ces observations que s'est cr\'e\'e un groupe de recherche sur Delannoy, qui s'est d'abord int\'eress\'e \`a la vie propre de Delannoy, puis \`a la communaut\'e des combinatoriciens et th\'eoriciens des nombres entre 1870 et 1914.\ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Perspectives de recherche} Nous comptons poursuivre nos efforts de recherche dans les directions actuelles : logique linéaire et applications (complexité implicite, planification, programmation logique), programmation et web, S-mots. En particulier, le programme de recherche portant sur la complexité implicite reste encore largement ouvert. Les problèmes d'expressivité ne sont pas totalement résolus et il conviendra de mieux savoir faire collaborer des approches différentes (approche par les quasi-interprétations par exemple) ou des cadres différents (circuits, complexité sur les réels). Le domaine de la programmation adaptée au web ouvre à des problématiques importantes (calcul concurrent avec données réparties, programmation avec données semi-structurées, programmation par partie).