Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision
Révision précédente
Prochaine révision Les deux révisions suivantes
fr:research:models-computation [2021/04/05 17:00]
apeiron
fr:research:models-computation [2021/04/05 17:05]
apeiron PLoopC
Ligne 1: Ligne 1:
  
  
-===== Thèse =====+====== Thèse ​======
  
  
-====== Résumé ​======+===== 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. 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.
Ligne 19: Ligne 19:
 **Mots-clés** : Algorithme séquentiel,​ ASM, calculabilité,​ complexité implicite, langage impératif, simulation, temps récursif primitif, temps polynomial. **Mots-clés** : Algorithme séquentiel,​ ASM, calculabilité,​ complexité implicite, langage impératif, simulation, temps récursif primitif, temps polynomial.
  
-====== Manuscrit ​======+===== Manuscrit =====
  
 **Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial** **Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial**
Ligne 30: Ligne 30:
 Voici {{:​manuscrit-these.pdf|la version finale}}. Voici {{:​manuscrit-these.pdf|la version finale}}.
  
-====== Soutenance ​======+===== Soutenance =====
  
 J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil. Voici {{ :​undefined:​soutenance.pdf | les slides}}. J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil. Voici {{ :​undefined:​soutenance.pdf | les slides}}.
Ligne 43: Ligne 43:
 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.
  
-====== Publications ​======+===== Publications =====
  
 Ce travail de thèse a donné lieu à deux publications : Ce travail de thèse a donné lieu à deux publications :
   * [[fr:​research:​fi-while|Algorithmic Completeness of Imperative Programming Languages]] (Yoann Marquer), accepté par Fundamenta Informaticae en 2016   * [[fr:​research:​fi-while|Algorithmic Completeness of Imperative Programming Languages]] (Yoann Marquer), accepté par Fundamenta Informaticae en 2016
   *  [[fr:​research:​ploopc|Imperative Characterization of Polynomial Time Algorithms]] (Yoann Marquer, Pierre Valarcher), publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130   *  [[fr:​research:​ploopc|Imperative Characterization of Polynomial Time Algorithms]] (Yoann Marquer, Pierre Valarcher), publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130
 +
 +====== While ======
 +
 +**Algorithmic Completeness of Imperative Programming Languages** (Yoann Marquer) est un article directement issu de [[fr:​research:​thesis-defense|mes travaux de thèse]], et qui a été accepté par Fundamenta Informaticae en 2016.
 +
 +===== Abstract =====
 +
 +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 ((Loïc Colson: "About primitive recursive algorithms",​ Theoretical Computer Science 83 (1991) 57–69)) and ((Yiannis N. Moschovakis:​ "On Primitive Recursive Algorithms and the Greatest Common Divisor Function",​ Theoretical Computer Science (2003) ))) 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 ((Yuri Gurevich: "​Sequential Abstract State Machines Capture Sequential Algorithms",​ ACM Transactions on Computational Logic (2000) ))) 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.
 +
 +===== Versions =====
 +
 +The {{:​fr:​research:​fi-while-short.pdf|short version}} of the paper had been submitted to [[http://​fi.mimuw.edu.pl/​index.php/​FI|Fundamenta Informaticae]].
 +
 +The {{:​fr:​recherche:​fi-while-long.pdf|long version}} is an older version, with very poor english and presentation,​ but contains proofs omitted in the short version.
 +
 +
 +====== PLoopC ======
 +
 +**An Imperative Language Characterizing PTIME Algorithms** (Yoann Marquer, Pierre Valarcher) est un article directement issu de [[fr:​research:​thesis-defense|mes travaux de thèse]], et qui a été publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130
 +
 +===== Abstract =====
 +
 +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.
 +
 +===== Versions =====
 +
 +Here is the {{:​en:​research:​ploopc2.pdf|submitted version}}.