Modèles de calcul

À la première section nous définirons les Abstract State Machines de Gurevich, et nous prouverons son théorème Algo = ASM pour obtenir une occurrence des algorithmes séquentiels (définis à la section 1.2) sous forme d’un modèle de calcul. Ainsi, un modèle de calcul M sera dit algorithmiquement complet si M peut simuler ASM. Par exemple dans [FZG10], Marie Ferbus-Zanda et Serge Grigorieff ont montré que le lambda-calcul non typé 1 est algorithmiquement complet, en acceptant la nature oraculaire des algorithmes.

En effet, pour chaque opération disponible un symbole de constante doit être ajouté au lambda-calcul afin que la simulation soit juste. Toutefois à la définition 2.3.5 p.56 nous n’insistons pas tant sur la simulation que sur la simulation mutuelle, afin de caractériser les classes algorithmiques. Mais pourquoi caractériser et pas seulement simuler ? Exemple 2.0.8. D’après le théorème d’ultime obstination de Colson [Col91], notre algorithme Min p.24 ne peut être implémenté dans le modèle de calcul de la récursion primitive, même si le minimum est une fonction primitive récursive. 

L’opérateur de minimisation µ est défini de la façon suivante : Soit f une fonction récursive (pouvant être partielle). µ[f] n’est définie sur ~n que s’il existe un x tel que f(~n, x) = 0, et que f(~n, i) est définie pour tout 0 ≤ i < x. Dans ce cas : µ[f](~n) =def min{x ∈ N | f(~n, x) = 0} En utilisant l’opérateur de minimisation sur la fonction caractéristique de F nous obtenons alors le résultat voulu : r = µ[1 − χF ](m, n) D’un point de vue impératif (voir la section 2.2), Min ne peut être obtenu avec un loop, mais peut l’être avec un while.

Ainsi, certes cet algorithme peut être implémenté dans un modèle strictement plus puissant, mais en temps que fonction récursive et plus en temps que fonction primitive récursive. La question est donc de déterminer la « clôture algorithmique » des fonctions primitives récursives, à savoir un modèle qui soit algorithmiquement complet mais qui ne donnerait que les fonctions primitives récursives.

David Michel et Pierre Valarcher l’ont trouvé dans [MV09] en assouplissant la condition de récursion. Dans un modèle impératif cela revient à utiliser des exceptions pour sortir des boucles loop. Ainsi, ils ont obtenu une caractérisation de APRA, l’ensemble des algorithmes séquentiels à temps primitif récursif et n’utilisant que les booléens et entiers unaires comme structure de données.

Les ASMs 

Rappel. Afin de définir correctement les ASMs, nous utilisons le fait que : 1. Tous les langages considérés sont égalitaire (voir p.18). 2. Les booléens sont introduits p.17, et les formules p.19. 3. La notion de mise à jour (f,~a, b) est introduite p.25. Définition 2.1.1. (Programme d’une ASM) Π =def f t1 . . . tα := t0 | if F then Π1 else Π2 endif | par Π1k . . . kΠn endpar où : 1. f est un symbole de fonction dynamique d’arité α 2.1. LES ASMS 37 2. t1, . . . , tα, t0 sont des termes du langage 3. F est une formule f t1 . . . tα := t0 sera appelée une commande de mise à jour.

Par la suite (notamment dans les preuves, pour simplifier les notations) il nous arrivera de noter u cette commande, et u X son interprétation (f,t1 X , . . . ,tα X ,t0 X ). Ainsi, u X est bien une mise à jour au sens défini p.25, et si u désigne une commande de mise à jour et non une mise à jour, nous continuerons à utiliser la notation X ⊕ u, mais cette fois pour signifier X ⊕ u X. Notation. Pour n = 0 une commande par Π1k . . . kΠn endpar est un programme « vide ». Si la partie else d’un programme if est par endpar alors nous écrirons simplement if F then Π endif.

Définition 2.1.2. (Termes lus et écrits par une ASM) L’ensemble Read(Π) des termes lus par Π et l’ensemble W rite(Π) des termes écrits par Π sont définis par induction sur Π : Read(f t1 . . . tα := t0) =def {t1, . . . , tα, t0} Read(if F then Π1 else Π2 endif) =def {F} ∪ Read(Π1) ∪ Read(Π2) Read(par Π1k . . . kΠn endpar) =def Read(Π1) ∪ · · · ∪ Read(Πn) À cause de la remarque p.28 nous ajouterons toujours true, false à Read(Π). W rite(f t1 . . . tα := t0) =def {f t1 . . . tα} W rite(if F then Π1 else Π2 endif) =def W rite(Π1) ∪ W rite(Π2) W rite(par Π1k . . . kΠn endpar) =def W rite(Π1) ∪ · · · ∪ W rite(Πn) Soit T(Π) =def Read(Π) ∪ Upd(Π). Définition 2.1.3. (Sémantique opérationnelle des ASMs) Un programme d’ASM Π induit une fonction de transition : τΠ(X) =def X ⊕ ∆(Π, X).