Ceci est une ancienne révision du document !


Résumé

Les fonctions calculables ont été formalisées par différents modèles de calcul (récursion, lambda-calcul, machines de Turing) ayant le même comportement entrées-sortie : c'est la thèse de Church. Par exemple, une machine de Turing à un ruban peut simuler les résultats calculés par une machine à deux rubans. Pourtant, pour la reconnaissance de palindrome la machine à un seul ruban nécessite une complexité en temps supérieure. Ainsi, il faut étudier les étapes intermédiaires. Nous définissons donc une simulation pas à pas entre exécutions, utilisant uniquement des variables temporaires et une dilatation temporelle.

La thèse de Church concernait donc les fonctions, et il nous faut une nouvelle thèse pour les algorithmes. Nous avons choisi celle de Gurevich pour sa présentation axiomatique : un algorithme séquentiel est un objet vérifiant les trois postulats de temps séquentiel, d'états abstraits et d'exploration bornée. De plus, il a montré que les algorithmes séquentiels coïncident avec son modèle des Abstract State Machines. Nous dirons donc qu'un modèle de calcul est algorithmiquement complet s'il existe une simulation mutuelle d'exécutions entre lui et les ASMs.

Pour obtenir des résultats sur des modèles de calcul plus usuels, nous formalisons les langages impératifs par un système de transition. En étudiant leur sémantique opérationnelle pas à pas et en développant une notion de graphe d'exécution, nous montrons qu'une variante du langage While de Jones est algorithmiquement complète. Ce résultat étant à structures de données près, il correspond donc à une équivalence entre les structures de contrôle des ASMs et des langages impératifs. De plus, étant préoccupés par la faisabilité des algorithmes, nous montrons que les structures du premier ordre utilisées par Gurevich permettent bien d'implémenter les structures de données usuelles.

Notre soucis de la faisabilité nous a également conduit à étudier en terme de complexité implicite deux restrictions des ASMs : celles en temps primitif récursif (les opérations usuelles et terminales) et celles en temps polynomial (les exécutions réalistes). Nous montrons d'une part que si les structures de données sont également primitives récursives, alors une variante LoopC du langage Loop de Meyer et Ritchie est complète pour les algorithmes en temps primitif récursif. D'autre part, une restriction syntaxique LoopCstat de LoopC est complète pour les algorithmes en temps polynomial, sans restriction sur les structures de données et en caractérisant syntaxiquement le degré du polynôme.

Mots-clés : Algorithme séquentiel, ASM, calculabilité, complexité implicite, langage impératif, simulation, temps récursif primitif, temps polynomial.

Manuscrit

Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial

Les rapporteurs ayant examiné mon manuscrit sont :

  • Patrick Baillot, directeur de recherche au CNRS
  • Gilles Dowek, directeur de recherche à INRIA
  • Daniel Leivant, professeur à l'Indiana University Bloomington

Voici la version finale.

Soutenance

J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil. Voici les slides.

Le jury était composé de :

  • Patrick Baillot, directeur de recherche au CNRS
  • Patrick Cégielski, professeur à l'Université Paris-Est Créteil
  • Gilles Dowek, directeur de recherche à INRIA
  • Jean-Yves Marion, président du jury et professeur à l'Université de Lorraine
  • Pierre Valarcher, mon directeur de thèse et professeur à l'Université Paris-Est Créteil

Ma soutenance a été filmée1), voici la vidéo postée sur ma chaîne.

Publications

Ce travail de thèse a donné lieu à deux publications :

  • Algorithmic Completeness of Imperative Programming Languages (Yoann Marquer), accepté par Fundamenta Informaticae en 2016
  • Imperative Characterization of Polynomial Time Algorithms (Yoann Marquer, Pierre Valarcher), publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130
1) Un grand merci à Marie Le Cun !