Summary in English at the end.

Théorie des algorithmes : étude comparée

La définition de la machine de Turing a permis de formaliser la notion de fonction calculable et l’essor de la calculabilité. Les algorithmes, notion bien plus ancienne que la notion de fonction calculable, n’ont été que très récemment formalisés à leur tour par la définition des Abstract State Machine (ASM) par Yuri Gurevich, célèbre logicien ainsi que par Yannis Moschovakis qui lui utilise les équations récursives (à la Mc Carthy).

Les travaux de Y. Gurevich ont plutôt mené à une formalisation axiomatique des différentes notions d’algorithmes (voire à la notion de classe d’algorithmes). Les ASM permettent de donner une définition formelle à tout algorithme séquentiel, indépendamment de la « machine » sur laquelle ils tournent, que ce soit les algorithmes usuels pour ordinateur séquentiel ou les algorithmes de géométrie effectués à la règle et au compas.

Alors que les machines de Turing permettent de décrire quelles fonctions sont calculables à l’aide d’un ordinateur, elles ne permettent pas de prendre en compte la dimension algorithmique du calcul. Par exemple, certains algorithmes ne peuvent pas être implantés fidèlement sur une machine de Turing (par exemple ceux ayant besoin d’un accès direct et non séquentiel à la mémoire). Les ASM permettent quant à elle de démontrer qu’un modèle de calcul est algorithmiquement complet, c’est-à-dire qu’il est capable de réaliser tout algorithme en respectant parfaitement chaque pas de calcul de l’algorithme.

Néanmoins, bien qu’elles soient un outil très intéressant, les ASM souffrent encore de quelques limitations :

• elles ne s’appliquent pas aux algorithmes parallèles. Il y a eu plusieurs tentatives pour faire une adaptation mais en générale, elles nécessitent plusieurs constructions très ad-hoc par rapport aux ASM séquentielles ;
• elles ne s’appliquent pas aux algorithmes non déterministes alors que beaucoup utilisent des générateurs de nombre pseudo aléatoire ou utilise de la mémoire non initialisée
• leur syntaxe est un peu rébarbative.

Les travaux de Y. Moschovakis, proviennent d’un résultat datant de la fin des années 1980 dû à L. Colson qui établie (via de la sémantique dénotationnelle) que certains algorithmes ne sont pas implémentables dans certains langages (alors que la fonction calculée par les algorithmes sont implémentables mais par d’autres algorithmes). Même si le résultat a été obtenu en étudiant le comportement intentionnel des algorithmes c’est via la complexité qu’il a été publicisé. Y. Moschovakis et L. van den Dries ont généralisé ce résultat, seulement en étudiant la complexité, et établissant des propriétés sur la complexité minimale de certains problèmes.

Le travail consiste à s’approprier les deux approches et à faire des liens entre elles mais on pourra aussi répondre à des questions plus spécifiques :

• définir les ASM par une définition exclusivement basée sur la logique : une ASM, au lieu d’être un programme, sera simplement définie par une formule logique. Il faudra, une fois l’équivalence avec les ASM séquentiels établie pour un certain type de formule,
• d’étudier les variantes parallèles, non-déterministes et à temps ordinal et obtenir un théorème équivalent à l’universalité algorithmique des ASM.
• avoir une approche axiomatique de la définition des algorithmes à la Moschovakis
• avoir une approche en terme de classe d’algorithmes dans le cadre des algorithmes de Moschovakis

Localisation : LACL, université Paris-Est Créteil
Encadrant : Julien Cervelle

Bibliographie :
https://www.math.ucla.edu/~ynm/lectures/aricplace/c-aric.pdf
https://web.eecs.umich.edu/~gurevich/Opera/141.pdf
http://bulletin.eatcs.org/index.php/beatcs/article/download/70/66

Summary in English

The definition of Turing machine made possible to formalize the notion of computable function and gave birth to computability. Algorithms, a concept much older than the concept of computable function, were only recently formalized by the definition of Abstract State Machine (ASM) by Yuri Gurevich, famous logician, as well as by Yannis Moschovakis who uses recursive equations (à la Mc Carthy).

The work consists in assimilate the two approaches and make links between them. We will also address more specific questions:

• Define ASMs by a definition exclusively based on logic: an ASM, instead of being a program, will simply be defined by a logical formula. It will be necessary, once the equivalence with the sequential ASMs established for a certain type of formula,
• To study parallel, non-deterministic and ordinal-time variants and obtain a theorem equivalent to the algorithmic universality of ASMs.
• Have an axiomatic approach to the definition of Moschovakis algorithms
• Have an approach in terms of class of algorithms within the framework of Moschovakis algorithms