J'ai été formé au lambda-calcul au master Logique Mathématique et Fondements de l'Informatique de l'Université Paris-Diderot. Mon stage de M2 avec le professeur émérite Jean-Louis Krivine porta sur une extension de la correspondance preuve/programme à la logique classique, en ajoutant des commandes comme callcc au lambda-calcul. Cette approche m'intéressa particulièrement car elle permet de donner un sens calculatoire aux théorèmes prouvés par les mathématiciens.

J'ai travaillé durant la première partie de ma thèse avec le professeur Tristan Crolard sur une traduction dans le système T des commandes de continuation comme callcc} manipulant les contextes pour forcer syntaxiquement les stratégies d'évaluation des programmes. En m'inspirant des travaux de Serge Grigorieff et Pierre Valarcher et des machines de Krivine, j'ai construit une représentation des stratégies contextuelles (par nom, par valeur et par besoin) du lambda-calcul sous forme d'Abstract State Machine (ASM).

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.

Ce travail est issu de mon stage postdoctoral³⁾ de fin 2015 à fin 2016. J'ai travaillé avec Jean-Baptiste Yunès et Luidnel Maignan au LIAFA sur le problème de la synchronisation dans les automates cellulaires, le « Firing Squad Synchronization Problem ».

Pour l'instant nous n'avons implémenté en Coq que les résultats préliminaires, qui nous ont servi à déterminer à quel point les preuves devaient être détaillées pour être ensuite implémentées le plus facilement possible. La preuve de la correction des champs infinis est quasiment terminée et est disponible sur HAL.

Le but est de concevoir un automate cellulaire (où chaque cellule ne peut communiquer qu'avec ses voisins) démarrant avec quelques cellules actives (les généraux) tel qu'au bout d'un moment toutes les cellules passent dans le même état simultanément (le peloton d'exécution fait feu). Beaucoup de solutions particulières ont été conçues selon le nombre et le placement des généraux, ou la notion de voisinage utilisée, mais pas de solution suffisamment générale. L'approche de Jean-Baptiste Yunès et Luidnel Maignan consiste à décomposer le problème en champs infinis modulables pouvant être adaptés à différentes variations du problème et composés ensuite pour le résoudre. Ces champs infinis peuvent ensuite être réduits en un nombre fini d'états permettant de définir l'automate cellulaire associé.

Mon objectif était de prouver que cette approche très algorithmique du problème produit bien le résultat attendu, et ce en utilisant l'assistant de preuve Coq. L'intérêt pour mon projet de recherche était double. D'une part, mon travail de thèse a essentiellement consisté à étudier la complexité en temps ainsi que la taille des éléments, approche qui a été complétée durant mon postdoc par l'étude des problèmes de voisinage et de transmission de l'information dans l'espace. D'autre part, mon style de preuve « mécanique » et mon intérêt pour la constructivité (en particulier la relation preuve/programme) étaient adaptés à une implémentation en Coq.

L'espace est simplifié pour la preuve : une cellule est un nombre entre et . Les champs sont définis récursivement sur le temps . Ainsi le champ Input, indiquant qu'une cellule est réveillée, est donné à par une fonction indiquant quels sont les généraux, puis se propage de proche en proche. Les autres champs (Border, Inside, Stable et Middle) sont de plus définis récursivement par couche, une couche au niveau servant à définir la couche suivante .

Tout d'abord nous avons prouvé la monotonie des champs, c'est à dire que le champ de distance ne peut qu'augmenter jusqu'à être stable, et pour les autres que quand un champ devient vrai il le reste. Puis nous avons caractérisé le moment où une région délimitée par deux bords et produit le cône de lumière permettant de faire apparaître le milieu de cette région.

Comme le milieu d'une région à une couche devient un bord à la couche , chaque région se divise en deux jusqu'à ce que toutes les cellules deviennent des bords. Cela définit notre champ Output.

Enfin, nous montrons que les milieux apparaissent en même temps pour chaque couche, ce qui nous permet de conclure qu'il existe une date à laquelle toutes les cellules émettent leur signal de sortie, et pas avant.

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).