Activité de l'équipe LIMD

Acronyme :

LIMD : "Logique, Informatique et Mathématiques Discrètes"

Descriptif de l'équipe :

Initialement ancrée en logique et théorie de la démonstration, l’équipe s’est ouverte ces dernières années, ouverture actée par son renommage récent en LIMD en 2007. Le thème général est l’informatique mathématique, au sens du GDR du même nom : l’équipe développe des objets et méthodes mathématiques pour répondre à des problématiques issues des grandes questions informatiques.

Au sein de l’informatique mathématique, l’équipe se présente comme la réunion de deux pôles¹ avec leurs recherches propres et leur cohérence interne : logique de la programmation et mathématiques discrètes.

Les notions de calcul, de programme et d’algorithme sont centrales à ces thèmes et donnent son unité à l’équipe : il s’agit de recherches portant sur la notion même de calcul , mais aussi de recherches avec de forts aspects algorithmiques et de programmation.

Logique de la programmation

En théorie de la démonstration et programmation, notre activité s’étend des fondements à l’implantation d’un langage de programmation expérimental, PML, qui permet de démontrer des propriétés sur les programmes. Côté fondements, nos travaux portent d’abord sur la correspondance de Curry-Howard entre démonstrations et programmes, ainsi que sur son extension à la réalisabilité. Plus généralement, nous travaillons sur les langages de programmation, de leur spécification à leur compilation. Un objet mathématique central à ces travaux est le λ-calcul de Church.

Travaux représentatifs de ce pôle

Tom Hirschowitz et Xavier Leroy, Mixin modules in a call-by-value setting, ACM Transactions on Programming Languages and Systems, 27(5) :857-881, 2005
Cet article, version journal de l’article du même nom, présente une solution au problème du typage des modules mixins. Il contient aussi la première interprétation en appel par valeur des modules mixins en termes de définitions récursives.
Peter Hancock et Pierre Hyvernat, Programming interfaces and basic topology, Annals of Pure and Applied Logic, Volume 137, Issues 1-3 : 189-239, 2006
La topologie formelle est une approche constructive de la topologie classique. Dans un tout autre registre, la notion de « système d’interaction » sert à formaliser la programmation par composants. Cet article relie les deux mondes (topologie / programmation) en montrant une équivalence de catégorie entre les espaces de la topologie formelle avec fonctions continues et les interfaces avec simulations.
René David et Karim Nour, An arithmetical proof of the strong normalization for the lambda-calculus with recursive equations on types, TLCA 2007, LNCS 4583 : 84-101, 2007
Cet article donne une preuve purement combinatoire de la forte normalisation du lambda calcul simplement typé où l’on autorise des équations mutuellement récursives sur les types satisfaisant les conditions de Mendler (conditions dont il avait montré le coté nécessaire et suffisant pour la forte normalisation). La preuve de forte normalisation de Mendler utilisait les candidats de réductibilité et n’était pas formalisable au premier ordre. Notre preuve montre donc que la force du système considéré est plus faible que celle de l’arithmétique de Peano.
Christophe Raffalli Realizability of the axiom of choice in HOL. (An analysis of Krivine’s work), Fundamenta Informaticae vol. 84 tome 2, 241-258, 2008
Cet article est une introduction aux travaux récents en réalisabilité et principalement le travail de Jean-Louis Krivine sur la réalisation de l’axiome du choix. Nous montrons aussi comment optimiser les programmes extraits en distinguant les formules avec et sans contenu algorithmique, car dans le cadre de la réalisabilité classique, il faut prendre quelques précautions par rapports aux techniques d’optimisations qui existent déjà dans le cas intuitionniste.
Christophe Raffalli et Pierre Hyvernat PML et ses motivations
PML est à la fois un langage de programmation fonctionnel et un outil d’aide à la démonstration, doté d’un langage commun de programmation, de typage et de preuve. Cette unification transgresse les paradigmes standard de proofs as programs et propositions as types, les remplaçant par programs as types and propositions and proofs.

Mathématiques discrètes

Nos recherches en mathématiques discrètes se fédèrent largement autour d’un même type d’objets (images, mots finis ou infinis, configurations, pavages, sous-shifts), mais avec des problématiques différentes allant de la compréhension géométrique de ces objets à l’étude de systèmes dynamiques agissant sur eux. Parmi les outils utilisés dans ces recherches, la combinatoire des mots (substitutions, suites Sturmiennes, droites discrètes, etc) a une place centrale. Par ailleurs, on retrouve un questionnement de fond sous-jacent à un grand nombre de nos travaux : comprendre les liens entre contraintes ou lois locales et configurations ou dynamiques globales.

Travaux représentatifs de ce pôle

Jacques-Olivier Lachaud, Anne Vialard, François de Vieilleville, Fast, accurate and convergent tangent estimation on digital contours, Image and Vision Computing, Volume 25, Issue 10 : 1572-1587, 2007
Nous présentons le premier estimateur géométrique local sur les contours discrets prouvé asymptotiquement convergent. Nous montrons qu’il se calcule en temps linéaire par rapport à la taille des données et qu’il est en pratique meilleur que les autres, même à basse échelle, sur différents critères (erreurs quadratiques moyenne et maximale, isotropie, conservation des propriétés de convexité, continuité).
G. Paquin et L. Vuillon, A characterization of balanced episturmian sequences, Electronic Journal of Combinatorics, Vol 14, no 1, Research Paper 33, 12 pp, 2007
Fraenkel prétend que le seul mot infini (sur k lettres) équilibré sur chacune de ses lettres et ayant des fréquences de lettres deux à deux distinctes est le mot infini (Fr_k)^ω tel que Fr_k = Fr_k−1 k Fr_k−1 avec Fr₃=1213121. Cette conjecture a maintenant 35 ans d’âge et un premier pas vers sa résolution a été fait grâce à l’étude des suites équilibrées données par suite directrice. Lors d’un séjour de trois mois à Montréal (Canada), L. Vuillon a finalisé l’article avec G. Paquin sur la conjecture de Fraenkel pour des mots périodiques épisturmiens. Ce résultat montre la conjecture de Fraenkel pour une sous-classe des suites équilibrées (qui généralisent les mots de Sturm i.e. les suites données par approximation discrète de droites dans le plan). C’est une avancée importante car nous pensons pouvoir nous ramener à cette sous-classe pour résoudre la conjecture.
L. Boyer et G. Theyssier On Local Symmetries and Universality in Cellular Automata, STACS 2009, 26th International Symposium on Theoretical Aspects of Computer Science, (electronic proceedings)
Nous avons montré pour diverses familles d’automates cellulaires définies par symétries locales, que la densité de l’universalité intrinsèque dans la famille est 1. Une des avancées significatives est d’avoir obtenu ce résultat de densité pour n’importe quelle façon de faire tendre le couple nombre d’états/rayon vers l’infini. Les hypothèses de symétries locales sont également très simples et pour certaines (automates totalistiques) très étudiées dans la littérature.

1: Il faut ajouter à ces deux pôles l’activité de recherche de R. Bonnet (prof. émérite).