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
fr:research:models-computation [2021/04/05 17:00]
apeiron
fr:research:models-computation [2021/04/07 11:41] (Version actuelle)
apeiron automates cellulaires
Ligne 1: Ligne 1:
 +Durant ma thèse j'ai prouvé des équivalences entre modèles de calcul en utilisant une simulation mutuelle, mettant en pratique l'​identité des indiscernables.
 +J'ai caractérisé des classes temporelles d'​algorithmes en utilisant des restrictions syntaxiques sur les langages de programmation impératifs,​ garantissant ainsi la complexité implicite des codes développés.
 +Durant mon premier postdoc j'ai utilisé les automates cellulaires pour mieux comprendre la propagation de l'​information dans l'​espace et pour me familiariser avec les assistants de preuve, afin d'​établir une garantie de correction pour l'​algorithme utilisé.
 +Puis j'ai étendu mes résultats de thèse au calcul parallèle utilisé dans la communauté HPC (High-Performance Computing), afin de capturer des paradigmes de communication entre processeurs.
  
  
-====== Thèse ======+====== Lambda-calcul ====== 
 + 
 +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). 
 + 
 + 
 +===== Réalisabilité classique ===== 
 + 
 +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  
 +{{ :​fr:​research:​realizability_in_classical_logic.pdf |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 $\mathtt{callcc}$) à 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 {{ :​fr:​research:​expose_krivine.pdf |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. 
 + 
 + 
 +===== Système T avec opérateurs de contrôle===== 
 + 
 +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 $\lambda \mu$-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 $\mathtt{let}$,​ 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 $\mathtt{callcc}$,​ $\mathtt{catch}$ ou $\mathtt{throw}$,​ mais le départ de Tristan Crolard mit le projet en sommeil. Voici ma {{ :​fr:​research:​tc3.pdf |dernière version}} de travail. 
 + 
 +===== Contenu algorithmique des stratégies du lambda-calcul ===== 
 + 
 +Les EMAs ont été développées notamment par Serge Grigorieff et Pierre Valarcher dans [[https://​arxiv.org/​abs/​1001.2160|leur article]]. L'​idée est que certes les Abstract State Machines de Gurevich peuvent simuler étape par étape toutes les machines usuelles((En tout cas, les machines dont le calcul est séquentiel,​ comme les machines de Turing ou les RAMs.)), 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 : 
 +$$\begin{array}{r|l@{}c@{}r@{}rcl@{}c@{}r@{}rc} 
 +\text{appel par nom} 
 +&{} \mu &​{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{} \mu, \mathunderscore &​{}\ \star\ &{} t_1 \ \star\ &{} t_2,​\pi \\ 
 +&{} \mu, \mathunderscore &​{}\ \star\ &{} \lambda x.t_1 \ \star\ &{} t_2,\pi &{} \succ &{} \mu &​{}\ \star\ &{} t_1[t_2/x] \ \star\ &{} \pi \\ 
 +\hline 
 +\text{appel par valeur} 
 +&{} \mu &​{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{} \mu, t_1 &​{}\ \star\ &{} t_2 \ \star\ &{} \mathunderscore,​\pi \\ 
 +&{} \mu, t &​{}\ \star\ &{} v \ \star\ &{} \mathunderscore,​\pi &{} \succ &{} \mu, \mathunderscore &​{}\ \star\ &{} t \ \star\ &{} v, \pi \\ 
 +&{} \mu, \mathunderscore &​{}\ \star\ &{} \lambda x.t \ \star\ &{} v,\pi &{} \succ &{} \mu &​{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\ 
 +\hline 
 +\text{appel par besoin} 
 +&{} \mu &​{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &​{}\mu,​ \mathunderscore &​{}\ \star\ &{} t_1 \ \star\ &{} t_2,​\pi \\ 
 +&{} \mu, \mathunderscore &​{}\ \star\ &{} v \ \star\ &{} t, \pi &{} \succ &{} \mu, v &{}\ \star\ &{} t \ \star\ &{} \mathunderscore,​\pi \\ 
 +&{} \mu, \lambda x.t &​{}\ \star\ &{} v \ \star\ &{} \mathunderscore,​\pi &{} \succ &{} \mu &​{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\ 
 +\end{array}$$ 
 + 
 +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 $n$ substitutions,​ alors la  machine ne contenant que ce terme((C'​est à dire que l'​antipile $\mu$ et la pile $\pi$ sont vides.)) fait des transitions jusqu'​à arriver à la même valeur en ayant fait exactement $n$ substitutions puis s'​arrête. Puis nous traduisons ces machines sous forme d'EMA, et discutons des généralisations possibles. 
 + 
 +Voici {{ :​fr:​research:​lema.pdf |la dernière version}}. 
 + 
 +====== Algorithmes séquentiels ====== 
 + 
 +====== Algorithmes parallèles ====== 
 + 
 +====== Automates cellulaires ====== 
 +Ce travail est issu de mon stage postdoctoral((Financé par l'ANR TARMAC 12 BS02 007 01.)) de fin 2015 à fin 2016. J'ai travaillé avec Jean-Baptiste Yunès et Luidnel Maignan au [[http://​archives.liafa.univ-paris-diderot.fr|LIAFA]] sur le problème de la synchronisation dans les automates cellulaires,​ le << Firing Squad Synchronization Problem >>. 
 + 
 +===== Versions ===== 
 + 
 +Pour l'​instant nous n'​avons implémenté {{ :​fr:​research:​fssp-coq-13.rar |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 [[https://​hal.archives-ouvertes.fr/​hal-01739317|HAL]]. 
 + 
 +===== Contexte du problème ===== 
 + 
 +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 [[http://​dl.acm.org/​citation.cfm?​id=2570381|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 [[http://​web.a.ebscohost.com/​abstract?​direct=true&​profile=ehost&​scope=site&​authtype=crawler&​jrnl=15575969&​AN=117653073&​h=q0DsSB07qQtTr4ExSbZ4utEFNt8pqrv1Ls9objyAD1h3DtaCaiZGkx%2bFy27SIic6ojlW71wBvftuB1UaubpLzA%3d%3d&​crl=c&​resultNs=AdminWebAuth&​resultLocal=ErrCrlNotAuth&​crlhashurl=login.aspx%3fdirect%3dtrue%26profile%3dehost%26scope%3dsite%26authtype%3dcrawler%26jrnl%3d15575969%26AN%3d117653073|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. 
 + 
 +===== Esquisse de la preuve ===== 
 + 
 +L'​espace est simplifié pour la preuve : une cellule $c$ est un nombre entre $1$ et $n$. Les champs sont définis récursivement sur le temps $t$. Ainsi le champ Input, indiquant qu'une cellule est réveillée,​ est donné à $t=0$ 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 $\ell$ servant à définir la couche suivante $\ell+1$. 
 + 
 +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 $b_1$ et $b_2$ 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 $\ell$ devient un bord à la couche $\ell+1$, 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. 
 + 
 + 
 + 
 + 
 +====== Thèse ​(TODO maj) ======
  
  
Ligne 48: Ligne 139:
   * [[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}}.
 +
 +
 +====== BSP ======
 +
 +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.
 +
 +===== Versions =====
 +
 +**An ASM Thesis for BSP** (Yoann Marquer, Frédéric Gava), le {{ :​fr:​research:​bsp-asm.pdf |premier rapport technique}},​ est disponible sur [[https://​hal.archives-ouvertes.fr/​hal-01717647|HAL]].
 +
 +**Algorithmic ​ Completeness of BSP Languages** (Yoann Marquer, Frédéric Gava), le {{ :​fr:​research:​bsp-while.pdf |second rapport technique}},​ est disponible sur [[https://​hal.archives-ouvertes.fr/​hal-01742406|HAL]].
 +
 +
 +
 +===== Résumé =====
 +
 +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 [[fr:​research:​fi-while|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**((Voir l'​article de Valiant : A Bridging Model for Parallel Computation)) 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 :
 +  - Chaque processeur effectue des calculs locaux, en n'​utilisant que les valeurs stockées dans sa propre mémoire.
 +  - Puis les processeurs envoient ou reçoivent des données.
 +  - 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 [[fr:​research:​fi-while|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).
 +