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/22 14:19]
apeiron
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.**\\ //(remove this paragraph once the translation is finished)//+====== The academic dissertation ====== 
 + 
 +**Imperative Characterization of Sequential Algorithms in general, primitive recursive or polynomial time** 
 + 
 +Here is {{:​manuscrit-these.pdf|the academic dissertation}}. 
 + 
 +====== 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. 
 + 
 +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. 
 + 
 +====== Thesis Defense ====== 
 + 
 +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.
Line 10: Line 30:
   * Pierre Valarcher, mon directeur de thèse et professeur à l'​Université Paris-Est Créteil   * Pierre Valarcher, mon directeur de thèse et professeur à l'​Université Paris-Est Créteil
  
-Ma soutenance a été filmée (un grand merci à Marie Le Cun !), voici [[https://​www.youtube.com/​watch?​v=Nx7ZDE7vV-c|la vidéo]] postée sur ma chaîne+Ma soutenance a été filmée((Un grand merci à Marie Le Cun !)), voici [[https://​www.youtube.com/​watch?​v=Nx7ZDE7vV-c|la vidéo]] postée sur ma chaîne.
- +
-Mon manuscrit est disponible en cliquant {{:​manuscrit-these.pdf|ici}}.+