Équipe « Logique, calcul et programmation »

Membres - Publications

Alexis Bes, Patrick Cegielski, Julien Cervelle, Luidnel Maignan, Pierre Valarcher, Serghei Verlan

Le premier but de cette thématique est d'étudier la puissance et le comportement de modèles de calculs parmi les ASM (abstrait state machine), les automates cellulaires, les systèmes de réécriture ou les systèmes à membrane.

L'une des questions les plus naturelles qui se posent concerne la décidabilité. En effet, par essence d'un modèle de calcul, la plupart des propriétés de ses calculs ou sur ses machines sont indécidables. Il est donc naturel de rechercher ce qui rend un modèle de calcul indécidable afin d'essayer, au travers de simplifications ou de restriction, de décrire la frontière avec le décidable. Plusieurs approches sont envisagées. L'une d'elle consiste à décrire le modèle avec une théorie logique et d'affaiblir cette dernière soit en réduisant la puissance des prédicats soit en choisissant des logiques plus faibles. Une autre consiste à limiter directement les possibilités du système en contraignant les transitions possibles.

Une autre question fondamentale est de savoir si un modèle de calcul est adapté à la modélisation de systèmes. On parle alors d'expressivité. Par exemple, si les machines de Turing sont reconnues comme étant le bon modèle pour les fonctions calculables, les ASM peuvent se révéler un meilleur modèle pour les algorithmes, c'est-à-dire là où la complexité entre en jeu. De même, la modélisation des systèmes physiques se fait essentiellement par des équations différentielles. Il est cependant intéressant d'étudier comment d'autres modélisations discrètes peuvent se révéler plus pertinentes dans les systèmes complexes ou chaotiques.

Emmanuel Polonowski, Pierre Valarcher

Nous étudions un nouveau formalisme de preuve de programmes impératif qui s'appuie sur des techniques issues de la théorie des types. Un des objectifs majeurs consiste à définir un cadre formel pour certifier des programmes impératifs et fonctionnels d'ordre supérieur utilisant des mécanismes de contrôle de flot (comme les sauts non-locaux, les continuations délimitées et les coroutines).

Les “logiques de programmes” (program logics) pour les langages impératifs prennent généralement la forme d'une “sémantique axiomatique” dans la lignée des travaux de Floyd, Hoare et Dijkstra. En comparaison, les logiques de programmes pour les programmes fonctionnels sont plus souvent basées sur l'interprétation des programmes comme des preuves (isomorphisme de Curry-Howard) qui est le fondement de la théorie des types.

Relativement peu de ponts existent entre ces deux mondes, et il est donc difficile d'exploiter des résultats obtenus en théorie des types dans le monde des logiques de programmes. Une avancée récente remarquable en théorie des types consiste en l'interprétation de mécanismes de contrôle génériques comme contenu calculatoire de raisonnements classiques (les théories des types étant traditionnellement constructives). L'intérêt de cette interprétation est en particulier d'être compatible avec la présence de variables procédurales d'ordre supérieur, cette combinaison étant par ailleurs réfractaire à l'axiomatisation sous forme de logique de Floyd-Hoare.

Le cadre formel que nous avons développé a donc pour but d'unifier ces deux points de vue afin de faire profiter les langages impératifs de ces résultats récents de théorie des types. Il peut être vu comme une théorie des types impérative classique, qui est assez expressive pour prendre en compte des sauts non-locaux et où il est donc possible d'interpréter les programmes impératifs bien typés directement comme des preuves classiques de leur spécification.

La sémantique dénotationnelle du langage impératif est au départ définie sous forme d'une traduction compositionnelle. Cette sémantique peut ensuite être raffinée en une sémantique opérationnelle qui sera simulée par la réduction de son image fonctionnelle, ou plus finement, par une machine abstraite. Le système de type dépendants du langage impératif est lui-même suffisamment riche pour autoriser le plongement d'une logique de Floyd-Hoare plus traditionnelle.

Luidnel Maignan, Olivier Michel, Antoine Spicher

L'émergence de nouvelles architectures matérielles (processeurs multi-coeurs, GPU, FPGA, grilles de calcul, réseaux/Internet) et des applications parallèles et distribuées qui les accompagnent, nécessitent l’évolution des modèles de calculs, des langages de programmation et le développement d’outils mieux adaptés. La programmation spatiale propose une façon originale d’attaquer cette problématique en étendant spatialement la notion de calcul. Suivant cette approche, l’espace peut être utilisé comme :

• support : plusieurs calculs peuvent s’effectuer simultanément mais à des positions différentes ; les données du calcul se déplacent sur l’espace et peuvent interagir lorsqu’elles se rencontrent ;
• résultat : l’espace se construit/se modifie au fur et à mesure du calcul en fonction des différentes interactions ; cette approche, bien que non-conventionnelle, convient à de nombreuses

applications (e.g., construction d’arbre couvrant dans les graphes dynamiques pour des protocoles pair-à-pair ou reconfiguration dynamique de FPGA).

La métaphore spatiale consiste donc à voir un calcul comme un système complexe, c’est-à-dire un système dynamique composé d’une multitude d’éléments pouvant interagir à travers une relation de voisinage. Le comportement global de ce type de système est particulièrement difficile à appréhender.

Le projet MGS développe un langage de programmation expérimental fondé sur des notions issues de la topologie algébrique. MGS permet la représentation d’organisations sophistiquées entre des entités variables et hétérogènes, ainsi que leur transformation par des règles locales (interactions). La structure de données fondamentale en MGS est la collection topologique. Une collection topologique est un ensemble d’éléments organisés par une relation de voisinage. Plus formellement, une collection considère un espace topologique discret décrit à l’aide d’un complexe cellulaire abstrait (concept étendant les graphes à des dimensions arbitraires) décoré par des valeurs. Une transformation est une structure de contrôle dédiée à la manipulation des collections topologiques. C’est aussi une fonction définie par cas où chaque cas est une règle de réécriture → . En partie gauche, est un motif spécifiant une sous-collection (i.e., un ensemble de contraintes structurelles et de gardes logiques) ; la partie droite est une expression évaluant une nouvelle sous-collection. L’application d’une règle sur une collection C consiste à identifier une sous-région A de C respectant les contraintes données par , à calculer une nouvelle sous-collection B à partir de , pour finalement remplacer B en lieu et place de A dans C. Ce mécanisme s’appelle la réécriture topologique.

Le paradigme de calcul offert par MGS permet de généraliser un grand nombre de modèle de calcul existant et s’appliquant à la programmation spatiale : la CHAM, les L systèmes, les P systèmes, les automates cellulaires, les machines à signaux, etc. Le langage MGS permet également la spécification élégante d’algorithmes ou la modélisation de phénomènes complexes (notamment en biologie du développement et en biologie synthétique).

Nathalie Caspard

En tant que relations d'ordre particulières - car définissables algébriquement - les treillis ont été considérés dès la fin du XIXè siècle par Schröder et Dedekind puis sont tombés dans l'oubli avant de reparaître dans les années 1930 grâce notamment à Birkhoff, Öre et bien d'autres mathématiciens. Ce furent longtemps les principaux ordres étudiés, en partie du fait de leurs liens avec l'algèbre universelle. Historiquement, leur étude précède celle des ordres.

Au sein de la théorie des treillis, nos recherches se sont orientées essentiellement sur les treillis finis et, plus particulièrement, sur ceux qui peuvent être construits à partir du treillis à 1 élément par une suite finie d'une opération appelée la duplication d'intervalle. Il a été montré que ces treillis sont exactement les treillis bornés définis algébriquement par McKenzie. Nous avons pu, entre autres, démontrer que certaines grandes classes connues de treillis finis sont de ce type (par exemple les treillis des permutations et même, plus généralement, les treillis associés aux groupes de Coxeter finis, certains treillis de fermetures,…). Nous étudions les propriétés structurelles et algorithmiques des treillis, et tentons d'établir des liens entre ces propriétés et des aspects applicatifs étudiés par d'autres collègues, que ce soit en représentation des connaissances, en bases de données, en théorie du consensus ou dans certains domaines de la physique.