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:02]
apeiron while
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.