Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
en:research:thesis-defense [2016/03/23 13:54]
apeiron removed
en:research:thesis-defense [2018/02/16 01:25] (current)
Line 1: Line 1:
-FIXME **This page is not fully translated, yet. Please help completing the translation.**\\ +====== ​The academic dissertation ​======
- +
-====== ​Le manuscrit ​======+
  
 **Imperative Characterization of Sequential Algorithms in general, primitive recursive or polynomial time** **Imperative Characterization of Sequential Algorithms in general, primitive recursive or polynomial time**
  
-Voici {{:​manuscrit-these.pdf|le manuscrit}} de thèse. +Here is {{:​manuscrit-these.pdf|the academic dissertation}}.
- +
-====== 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.+====== Abstract ======
  
 +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.
  
-La thèse de Church ​concernait donc les fonctionset il nous faut une nouvelle thèse pour les algorithmesNous 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équentield'​états abstraits et d'exploration ​bornéeDe plusil 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.+Church's thesis therefore concerns functionsand we need a new thesis for algorithmsWe chose Gurevich's thesis for its axiomatic presentationa sequential algorithm is an object satisfying the three postulates of sequential timeabstract states and bounded ​exploration. ​Moreoverhe 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.
  
-Pour obtenir des résultats sur des modèles de calcul plus usuels, nous formalisons les langages impératifs par un système de transitionEn étudiant leur sémantique opérationnelle pas à pas et en développant une notion de graphe d'​exécutionnous montrons qu'une variante du langage While de Jones est algorithmiquement complète. Ce résultat étant à structures ​de données prèsil correspond donc à une équivalence entre les structures de contrôle des ASMs et des langages impératifsDe plusétant préoccupés par la faisabilité des algorithmesnous montrons que les structures du premier ordre utilisées par Gurevich permettent bien d'​implémenter les structures ​de données usuelles.+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)Firstlywe prove that if the data structures ​are also primitive recursivethen a variant LoopC of Meyer and Ritchie'​s language is complete for the algorithms in primitive recursive timeSecondlywe prove that a syntactical restriction LoopCstat of LoopC is complete for the algorithms in polynomial timewithout 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.
  
-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.+====== Thesis Defense ======
  
-====== Soutenance ======+FIXME **This page is not fully translated, yet.**
  
 J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil. J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil.