Durant ma deuxième année de master Logique Mathématique et Fondements de l'Informatique en 2011, je profitais de ma présence à l'Université Paris-Diderot pour faire mon stage auprès du professeur émérite Jean-Louis Krivine. Il m'avait impressionné par sa démarche tentant d'associer un contenu calculatoire à tous les résultats mathématiques, et il m'a fait travailler sur son article traitant de réalisabilité classique.

La logique intuitionniste peut être vue comme la logique classique où des règles équivalentes comme le tiers exclu, l'élimination de la double négation ou la loi de Peirce ne seraient plus toujours autorisées. La correspondance de Curry-Howard permet d'associer à chaque preuve en logique intuitionniste un programme en lambda-calcul. En cherchant à typer une instruction de contrôle dans un langage dérivant du lambda-calcul, l'informaticien Tim Griffin associa un programme (la commande ) à la loi de Peirce.

Ainsi, la correspondance de Curry-Howard peut être étendue à la logique classique. Plus formellement, étendons le lambda-calcul habituel avec une instruction cc pour « current continuation » en introduisant des piles e termes clos et des continuations comme termes. Alors il est possible de définir un système de transition, qui est un lambda-calcul avec continuations.

Jean-Louis Krivine va plus loin dans ce papier et les autres en associant des programmes aux axiomes de la théorie des ensembles et à l'axiome du choix, ce qui permet d'étendre la correspondance à tous les théorèmes prouvés depuis l'antiquité. Pour un résumé accessible de ses travaux, voir l'exposé de Krivine à un colloque de sciences cognitives.

Cette approche très constructive stimula mon intérêt pour les modèles de calcul, notamment implémentés sous forme de système de transition comme ce fût le cas durant ma thèse, ainsi que pour la correspondance preuve-programme, notamment lors de mon apprentissage de Coq durant mon postdoc.

Un des buts est d'étendre le lambda-calcul afin d'étendre la correspondance de Curry-Howard. La réalisabilité classique de Krivine ainsi que le -calcul de Parigot sont des avancées indépendantes dans cette direction. D'autres tentatives (par Nakano, Sato ou Kameyama par exemple) insistent sur l'aspect non-déterminisme de ces opérateurs de contrôle. Pour forcer le déterminisme, il faut forcer la stratégie d'évaluation, ce que nous faisons avec un lambda-calcul monadique où seules les valeurs (variables ou abstractions) peuvent être argument d'une réduction.

Afin d'inclure les entiers et la récurrence, c'est le système T de Gödel et non le lambda-calcul qui sera utilisé comme base. Nous obtenons donc un système T par valeur, que nous traduisons vers un système T « nommé » avec des , puis vers le système T habituel. En montrant la compatibilité de notre traduction avec la réduction habituelle, nous obtenons la normalisation forte de notre système de calcul en la dérivant de celle du système T.

L'idée aurait été ensuite d'ajouter à notre système de calcul des opérateurs de contrôle comme , ou , mais le départ de Tristan Crolard mit le projet en sommeil. Voici ma dernière version de travail.

Les EMAs ont été développées notamment par Serge Grigorieff et Pierre Valarcher dans leur article. L'idée est que certes les Abstract State Machines de Gurevich peuvent simuler étape par étape toutes les machines usuelles¹⁾, mais que simulation n'est pas identification. Ainsi, Serge Grigorieff et Pierre Valarcher montrent que des classes naturelles d'EMAs peuvent être littéralement identifiées à ces machines, ce qui fait des EMAs un modèle mathématique unificateur.

Dans cette optique, j'ai cherché à formaliser sous forme de machines abstraites les différentes stratégies d'évaluation contextuelle utilisées pour le lambda-calcul. Le terme à évaluer n'est donc qu'une entrée, et c'est la stratégie d'évaluation elle-même qui est vue comme un algorithme. Les différentes stratégies étudiées sont l'appel par nom, l'appel par besoin et l'appel par valeur, qui sont respectivement implémentées par la machine de Krivine et deux machines créées pour l'occasion :

Nous prouvons que nos machines sont correctes, c'est à dire que si un terme est évalué avec une stratégie jusqu'à une valeur finale en substitutions, alors la machine ne contenant que ce terme²⁾ fait des transitions jusqu'à arriver à la même valeur en ayant fait exactement substitutions puis s'arrête. Puis nous traduisons ces machines sous forme d'EMA, et discutons des généralisations possibles.

Voici la dernière version.

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.

La thèse de Church concernait donc les fonctions, et il nous faut une nouvelle thèse pour les algorithmes. Nous 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équentiel, d'états abstraits et d'exploration bornée. De plus, il 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.

Pour obtenir des résultats sur des modèles de calcul plus usuels, nous formalisons les langages impératifs par un système de transition. En étudiant leur sémantique opérationnelle pas à pas et en développant une notion de graphe d'exécution, nous montrons qu'une variante du langage While de Jones est algorithmiquement complète. Ce résultat étant à structures de données près, il correspond donc à une équivalence entre les structures de contrôle des ASMs et des langages impératifs. De plus, étant préoccupés par la faisabilité des algorithmes, nous montrons que les structures du premier ordre utilisées par Gurevich permettent bien d'implémenter les structures de données usuelles.

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.

Mots-clés : Algorithme séquentiel, ASM, calculabilité, complexité implicite, langage impératif, simulation, temps récursif primitif, temps polynomial.

Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial

Les rapporteurs ayant examiné mon manuscrit sont :

• Patrick Baillot, directeur de recherche au CNRS
• Gilles Dowek, directeur de recherche à INRIA
• Daniel Leivant, professeur à l'Indiana University Bloomington

Voici la version finale.

J'ai soutenu ma thèse en informatique le vendredi 9 octobre 2015 à Créteil. Voici les slides.

Le jury était composé de :

• Patrick Baillot, directeur de recherche au CNRS
• Patrick Cégielski, professeur à l'Université Paris-Est Créteil
• Gilles Dowek, directeur de recherche à INRIA
• Jean-Yves Marion, président du jury et professeur à l'Université de Lorraine
• Pierre Valarcher, mon directeur de thèse et professeur à l'Université Paris-Est Créteil

Ma soutenance a été filmée³⁾, voici la vidéo postée sur ma chaîne.

Ce travail de thèse a donné lieu à deux publications :

• Algorithmic Completeness of Imperative Programming Languages (Yoann Marquer), accepté par Fundamenta Informaticae en 2016
• Imperative Characterization of Polynomial Time Algorithms (Yoann Marquer, Pierre Valarcher), publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130

Algorithmic Completeness of Imperative Programming Languages (Yoann Marquer) est un article directement issu de mes travaux de thèse, et qui a été accepté par Fundamenta Informaticae en 2016.

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 ⁴⁾ and ⁵⁾) 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 ⁶⁾) 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.

The short version of the paper had been submitted to Fundamenta Informaticae.

The long version is an older version, with very poor english and presentation, but contains proofs omitted in the short version.

An Imperative Language Characterizing PTIME Algorithms (Yoann Marquer, Pierre Valarcher) est un article directement issu de mes travaux de thèse, et qui a été publié en 2016 dans Developments in Implicit Computational Complexity, volume 3, pages 91 - 130

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.

Here is the submitted version.

Ce travail a démarré fin 2016, et a été réalisé en collaboration avec Frédéric Gava, maître de conférences à l'Université Paris-Est Créteil. Bien qu'il n'ait pas été financé par contrat, j'ai été affilié au Laboratoire d’Algorithmique, Complexité et Logique pendant que j'exerçais mon activité de chercheur bénévole.

An ASM Thesis for BSP (Yoann Marquer, Frédéric Gava), le premier rapport technique, est disponible sur HAL.

Algorithmic Completeness of BSP Languages (Yoann Marquer, Frédéric Gava), le second rapport technique, est disponible sur HAL.

La thèse de Gurevich énonce que l'ensemble des algorithmes séquentiels sont capturés par ses trois postulats. De plus, il a prouvé que ces trois postulats définissent le même ensemble que ses Abstract State Machines. Ainsi, nous avons que ASM = Algo. Cela montre que l'approche axiomatique des postulats est équivalente à l'approche opérationnelle des ASMs.

Dans cet article, j'ai montré que les langages impératifs usuels sont non seulement Turing-complets mais aussi algorithmiquement complets. Cela a été fait en prouvant qu'un langage impératif minimal While est algorithmiquement équivalent aux ASMs de Gurevich. Ainsi, nous avons While ≃ ASM, ce qui signifie plus précisément que les exécutions des deux modèles de calcul sont les mêmes, à variables fraîches et dilatation temporelle près. Donc nous avons While ≃ Algo, ce qui montre que tout langage de programmation contenant les commandes de While est algorithmiquement complet (pour les algorithmes séquentiels).

Dans le contexte HPC (High Performance Computing), un résultat similaire paraît difficile à obtenir. Le problème principal est le manque de définition pour ce qu'est formellement un calcul HPC, ou dit autrement, la communauté HPC manque d'une définition consensuelle de ce qu'est la classe des algorithmes HPC. Utiliser un modèle pont⁷⁾ peut être vu comme un premier pas dans cette direction, qui fournit un pont conceptuel entre l'implémentation physique de la machine, et l'abstraction possible pour le programmeur. Cela simplifie également la tâche de la conception d'algorithme, leur programmation, et assure une meilleure portabilité d'un système à l'autre. Et, plus important encore, cela permet de raisonner sur le coût même des algorithmes.

Plus précisément, BSP (Bulk Synchronous Parallelism) est un modèle de programmation parallèle consistant en la séquentialisation de super-étapes divisées en trois phases :

1. Chaque processeur effectue des calculs locaux, en n'utilisant que les valeurs stockées dans sa propre mémoire.
2. Puis les processeurs envoient ou reçoivent des données.
3. Enfin, une barrière de synchronisation a lieu quand les communications sont terminées, et rend les données échangées disponibles aux mémoires locales des processeurs.

Le but est de rendre les programmes simples à écrire, indépendants des architectures, et que les performances d'un programme sur une architecture donné soit prévisible. Pour cela, les algorithmes BSP sont associés à un modèle de coût : le coût (en temps) d'une super-étape est w + h×g + l, où w est le nombre maximum de calculs fait par un processeur durant la super-étape, h est le nombre maximum de messages envoyés ou reçus, g mesure la perméabilité du réseau et l est le coût de la barrière de synchronisation.

Jusqu'à maintenant, il y a eu de nombreux langages de programmation ou bibliothèques pour programmer des algorithmes BSP, comme la BSPLIB pour le langage C ou Java, BSML, Pregel pour le big-data, etc. Mais pour l'instant il n'y a pas de définition explicite faisant consensus.

Notre but a été de faire un travail similaire à celui de Gurevich pour définir axiomatiquement les algorithmes BSP, de prouver que ces algorithmes peuvent être vus comme une extension naturelle du modèle des ASMs, et enfin de montrer une équivalence algorithmique de ces ASMs étendues avec un langage de programmation impératif. Ainsi, ce langage est caractéristique des algorithmes BSP, et peut être pris comme définition opérationnelle des algorithmes séquentiels.

Dans le premier rapport technique, nous avons axiomatisé l'ensemble Algo-BSP des algorithmes BSP en étendant les trois postulats de Gurevich d'un seul processeur à un p-uplet de processeurs travaillant simultanément, et en ajoutant un quatrième postulat pour tenir compte des super-étapes dans le modèle BSP, c'est à dire l'alternance dans un algorithme BSP entre phase de calcul (où les processeurs font leurs calculs de manière indépendante) et phase de communication.

Puis nous avons étendu le modèle de calcul ASM à des p-uplet de processeurs en appliquant le même programme ASM en même temps à chaque processeur durant les phases de calcul, et durant les phases de communication en supposant l'existence d'une fonction de communication abstraite (afin que le résultat ne dépende pas d'une implémentation particulière des communications). Nous avons prouvé que cette extension ASM-BSP est bien la contrepartie opérationnelle des algorithmes BSP définis de manière axiomatique, c'est à dire que ASM-BSP = Algo-BSP.

Comme dans mon article sur While nous pensons qu'un langage impératif est plus pratique qu'une simple fonction de transition pour déterminer des classe en temps ou en espace, ou tout simplement pour être comparé à des langages de programmation plus usuels. Ainsi, nous avons défini dans le deuxième rapport technique la sémantique opérationnelle d'un langage impératif minimal While-BSP travaillant sur des p-uplets de processeurs. Enfin, nous avons prouvé que While-BSP et ASM-BSP pouvaient se simuler l'un l'autre d'un point de vue algorithmique: While-BSP ≃ ASM-BSP.

De ces deux rapports techniques, nous pouvons donc déduire que While-BSP ≃ Algo-BSP, et donc que notre langage impératif minimal est bien algorithmiquement complet (pour les algorithmes BSP).