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.

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.

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ée¹⁾, voici la vidéo postée sur ma chaîne.

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

Algorithmic Completeness of Imperative Programming Languages (Yoann Marquer) est un article directement issu de mes travaux de thèse, et qui a été accepté par Fundamenta Informaticae en 2016.

According to the Church-Turing Thesis, effectively calculable functions are functions computable by a Turing machine. Models that compute these functions are called Turing-complete. For example, we know that common imperative languages (such as C, Ada or Python) are Turing complete (up to unbounded memory).

Algorithmic completeness is a stronger notion than Turing-completeness. It focuses not only on the input-output behavior of the computation but more importantly on the step-by-step behavior. Moreover, the issue is not limited to partial recursive functions, it applies to any set of functions. A model could compute all the desired functions, but some algorithms (ways to compute these functions) could be missing (see ²⁾ and ³⁾) for examples related to primitive recursive algorithms).

This paper's purpose is to prove that common imperative languages are not only Turing-complete but also algorithmically complete, by using the axiomatic definition of the Gurevich's Thesis and a fair bisimulation between the Abstract State Machines of Gurevich (defined in ⁴⁾) and a version of Jones' While programs. No special knowledge is assumed, because all relevant material will be explained from scratch.

Keywords: Algorithm, ASM, Completeness, Computability, Imperative, Simulation.

The short version of the paper had been submitted to Fundamenta Informaticae.

The long version is an older version, with very poor english and presentation, but contains proofs omitted in the short version.

An Imperative Language Characterizing PTIME Algorithms (Yoann Marquer, Pierre Valarcher) est un article directement issu de mes travaux de thèse, et qui a été publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130

Abstract State Machines of Y. Gurevich capture sequential algorithms, so we define the set of PTIME algorithms as the set of ASM programs computed in polynomial time (using timer-step principle). Then, we construct an imperative programming language PLoopC using bounded loop with break, and running with any data structure. Finally, we prove that PLoopC computes exactly PTIME algorithms in lock step (one step of the ASM is simulated by using a constant number of steps).

Keywords: ASM, computability, imperative language, implicit complexity, polynomial time, sequential algorithms, simulation.

Here is the submitted version.