Imperative Characterization of Sequential Algorithms in general, primitive recursive or polynomial time

Here is the academic dissertation.

Calculable functions were formalized by different computation models (recursion, lamb\-da calculus, Turing machines) with the same input-output behavior: this is the Church's Thesis. For example, a one-tape Turing machine can simulate the results computed by a two-tapes machine. However, for the palindrome recognition the one-tape machine requires a greater complexity in time. Thus, we must study the intermediate steps. So we define a step-by-step simulation between executions, using only temporary variables and time dilation.

Church's thesis therefore concerns functions, and we need a new thesis for algorithms. We chose Gurevich's thesis for its axiomatic presentation: a sequential algorithm is an object satisfying the three postulates of sequential time, abstract states and bounded exploration. Moreover, he proved that the sequential algorithms coincide with his model of Abstract State Machines. So we will say that a computation model is algorithmically complete if there exists a mutual simulation of executions between it and the ASMs.

To obtain results on more common computation models, we formalize imperative programming languages by a transition system. By studying their operational semantics step by step and developing a notion of graph of execution, we prove that a variant of Jones' language While is algorithmically complete. This result is up to data structures, so it corresponds to an equivalence between the control flow statements of the ASMs and the imperative languages. Moreover, being concerned for the feasibility of algorithms, we prove that the first order structures used by Gurevich enable the implementation of usual data structures.

Our concern for feasibility has also led us to study in terms of implicit complexity two restrictions of the ASMs: those in primitive recursive time (the usual and terminal operations) and those in polynomial time (the realistic executions). Firstly, we prove that if the data structures are also primitive recursive, then a variant LoopC of Meyer and Ritchie's language is complete for the algorithms in primitive recursive time. Secondly, we prove that a syntactical restriction LoopCstat of LoopC is complete for the algorithms in polynomial time, without restriction on the data structures and with a syntactical characterization of the degree of the polynomial.

Keywords: ASM, computability, implicit complexity, imperative language, polynomial time, primitive recursive time, sequential algorithm, simulation.

This page is not fully translated, yet.

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

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.