David Madore's WebLog: Un regard alternatif sur la réduction de Turing

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

↓Entry #2819 [older| permalink|newer] / ↓Entrée #2819 [précédente| permalien|suivante] ↓

(vendredi)

Un regard alternatif sur la réduction de Turing

Méta : Contrairement au précédent qui prétendait être de la vulgarisation (avec quel succès je ne sais pas), le présent billet s'adresse aux personnes qui ont déjà une certaine familiarité avec la calculabilité. (En gros, les prérequis sont les mêmes que dans ce billet ou celui-ci ou celui-là, qui sont sur des sujets proches : je suppose que les notions, disons, de machine universelle ou de codage de Gödel sont connues, et c'est préférable si la notion de machine avec oracle est aussi familière, même si je vais la redéfinir ci-dessous. Les billets que je viens de citer et celui-ci peuvent se lire indépendamment et dans n'importe quel ordre, mais ils devraient s'éclairer mutuellement puisque tout ceci tourne autour des mêmes questions.)

Désolé, donc, pour les gens qui espéraient un billet non technique et qui voient de nouveau de la calculabilité (surtout que j'ai mis beaucoup de temps à le publier parce que j'avais plein de choses à faire), mais j'ai compris quelque chose, là, et il est très utile pour moi de le coucher par écrit pour m'en souvenir ultérieurement.

Plan

Introduction non technique (pourquoi ce billet ?)

(On peut sauter cette section ainsi que la suivante si on veut entrer dans le vif du sujet.)

La motivation de ce billet est pour moi d'essayer de comprendre le sens d'un théorème et ce que nous apprend sa démonstration, et pourquoi je pense qu'il est intéressant et important. Le théorème en question n'est pas de moi : il est de Martin Hyland[#], mais je ne suis pas sûr que ça ait vraiment été remarqué qu'on pouvait le formuler de la manière que je vais expliquer, donc disons que le théorème est dû à Hyland mais la formulation est (peut-être) originale. Le théorème tel qu'écrit par Hyland parle de choses un peu sophistiquées (des « topologies de Lawvere-Tierney sur le topos effectif »), mais ce qui m'intéresse ici est qu'on peut le reformuler, ainsi que sa démonstration, de façon un peu plus élémentaire et peut-être plus « informatique ». Ce qui ne veut pas dire que la démonstration soit forcément facile à suivre pour autant ! En tout cas, je ne m'attends pas que le lecteur sache ce qu'est qu'une topologie de Lawvere-Tierney ni ce qu'est le topos effectif. Si vous voulez en savoir un peu plus sur ce que ces mots veulent dire (enfin, au moins les deux derniers), je renvoie aux autres entrées de ce blog liées ci-dessus, mais, je répète, ce n'est normalement pas nécessaire de les lire pour comprendre ce qui suit.

[#] L'article original de Hyland où se trouve ce théorème a pour titre The Effective Topos, et il est paru p. 165–216 dans les actes The L.E.J. Brouwer Centenary Symposium édité par Troelstra & van Dalen (1982) : en voici une version retypographiée et le scan de la version d'origine (disponible sur Sci Hub si vous n'y avez pas accès par ce lien). Le théorème en question est essentiellement une reformulation du théorème 17.2 de l'article en question (ou, disons, de l'ensemble de §17, parce que le lemme qui précède est également important dans ce que je raconte).

C'est, en fait, une tâche assez fréquente dans le travail d'un mathématicien d'essayer de « décoder » une démonstration (pas juste la vérifier, mais arriver à voir ce qu'elle devient dans un cas particulier, ou dans un cadre un peu différent, ou quand on l'applique dans tel ou tel contexte, ou quand on la traduit dans des termes plus élémentaires, ou quelque chose comme ça). Et ce qui suit est le résultat d'un tel travail de ma part, qui m'a pris, à vrai dire, un temps extrêmement embarrassant à mener[#2] (quelque chose comme trois mois, même si je n'ai évidemment pas consacré toute mon activité à ça), à cause du nombre de fois que je me suis embrouillé dans les notations et les programmes qui appellent un programme qui appelle un autre programme.

[#2] En fait, c'est même plus embarrassant que ça, parce que je n'ai pas réussi à vraiment décoder la démonstration donnée par Hyland : j'ai fini par laisser tomber et par trouver la mienne, et c'est celle-ci que je présente ci-dessous. Elle est problablement équivalente à celle de Hyland, parce que je l'ai trouvée en essayant de mettre ensemble les idées et l'inspiration que j'ai retenues de l'article de Hyland. Mais je n'en suis pas complètement certain non plus.

Mon but est donc d'enregistrer mon cheminement mental[#3], mais aussi d'essayer d'amener le lecteur à comprendre quelque chose que j'ai eu beaucoup de mal à comprendre, et, forcément, ceci présente un certain défi pédagogique, que je ne sais pas si je vais réussir à mener. (Peut-être que ce n'est pas possible d'expliquer certaines choses, qu'il faut forcément s'embrouiller soi-même avant de pouvoir se désembrouiller.) Je suis encore moins persuadé d'arriver à expliquer pourquoi je pense que c'est un théorème intéressant et important, mais je vais au moins essayer un peu. En revanche, je vais devoir demander à mon lecteur une certaine concentration, au moins pour la preuve du théorème, que je continue à trouver un peu cryptique à ce stade.

[#3] Les billets de mon blog sont souvent (cf. ici) principalement destinés à permettre à mon moi futur de retrouver le fil de mes pensées, donc j'explique un peu de façon à expliquer les choses à moi-même dans un avenir où j'aurais oublié comment tout ça fonctionne.

L'idée du théorème, donc, c'est qu'il nous donne une propriété équivalente à A est Turing-réductible à B (pour A,B⊆ℕ ; je vais rappeler ci-dessous ce que ça signifie, mais très rapidement ça signifie qu'on peut décider algorithmiquement si un entier appartient à A en ayant le droit de poser des questions sur l'appartenance de divers entiers à B). La propriété équivalente est celle de l'existence d'un convertisseur universel de B vers A (ce n'est pas un concept standard, et je vais le définir ci-dessous), qui est une sorte de méta-programme qui transforme un répondeur pour B en un répondeur pour A, eux-mêmes des concepts que je vais aussi définir et tenter d'expliquer (en gros ce sont des programmes qui répondent à la question de savoir si un élément appartient à B, resp. à A, mais ils y répondent de façon un peu tarabiscotée).

La notion de réduction de Turing est cruciale et centrale dans l'étude de la calculabilité, donc il est certainement bon de l'examiner avec attention. La propriété équivalente proposée par le théorème (cette notion de convertisseur universel) peut sembler compliquée et artificielle, mais je vais essayer d'argumenter qu'elle ne l'est pas tant que ça. Ce qui est intéressant avec cette propriété, c'est que même si elle est peut-être plus difficile à comprendre que la définition originale de la réduction de Turing, elle est aussi plus « pure » : on a besoin de savoir moins de choses pour l'écrire, et ces choses ne dépendent que très peu des détails de la théorie de la calculabilité.

Donc, d'abord, l'intérêt est de fournir une définition de la réduction de Turing qui ne fasse pas intervenir la notion d'« oracle » normalement utilisée pour la définir : savoir qu'on peut définir la réduction de Turing sans parler d'oracle (ou sans la déguiser de façon vraiment transparente) me semble, en soi, assez intéressant. Bon, je ne sais pas dans quelle mesure cette définition est vraiment utilisable comme définition (peut-être que pour montrer n'importe quoi dessus on va de toute façon devoir ressortir toute la théorie des oracles), mais c'est en soi surprenant qu'on puisse trouver un tel équivalent.

Mais l'intérêt est aussi que cette propriété équivalente se prête plus facilement à la généralisation : c'est peut-être plus compliqué, certes, mais on est essentiellement dans le domaine de la pure logique[#4], donc les notions ont un sens dans un contexte beaucoup plus large, et on peut se demander ce que ça donne dans un tel contexte.

[#4] En quelque sorte, tout le thème du billet (mais que je vais laisser caché en arrière-plan, et je n'en parle qu'en petits caractères, pour ne pas supposer de connaissances de logique intuitionniste) est de comprendre le sens de la formule logique ∀P:Ω. (((∃n:ℕ.(nB∨¬nBP)) ⇒ P) ⇒ ((∃m:ℕ.(mA∨¬mAP)) ⇒ P)) (ici, Ω est l'ensemble des valeurs de vérité) : l'équivalent dont je parle, c'est que cette formule est vérifiée [i.e., réalisable], dans le topos effectif, si et seulement si A est Turing-réductible à B. Et le sens de la remarque, c'est que cette formule (ainsi que des généralisations évidentes de celles-ci, notamment si on remplace A,B⊆ℕ par des sous-objets de n'importe quel objet, voire nB∨¬nB et mA∨¬mA par des prédicats quelconques sur n'importe quel objet) a un sens dans n'importe quel topos. (Son sens est la plus petite topologie de Lawvere-Tierney qui rend B décidable rend aussi A décidable, mais ce que montre ce billet, c'est qu'il est parfaitement possible que ceci se déchiffre de manière qui ne fasse pas appel à la notion de topologie de Lawvere-Tierney.)

Enfin, je trouve intéressant que cette approche fasse assez naturellement intervenir des notions fondamentales en informatique : le continuation-passing-style dans un sens (et, en fait, on peut dire que toute cette histoire est juste une réécriture des oracles en CPS ; sauf que la conversion dans l'autre sens n'est pas aussi facile que cette remarque le suggère), et, dans l'autre sens, la notion de monade. Je ne suis pas sûr d'avoir encore bien compris le sens profond de cette apparition, mais j'espère que le fait d'écrire ce billet m'aidera au moins à y voir plus clair.

Quelques notations et conventions

Cette section est là uniquement pour référence (et je l'ai écrite après le reste). Toutes les notations seront introduites au fur et à mesure de leur utilisation, ou bien sont assez standard ou évidentes, donc on peut sauter cette section (et peut-être qu'il vaut mieux le faire), mais c'est sans doute une bonne idée de les rassembler en un seul endroit pour référence.

D'abord, pour qu'elles soient plus commodes à retrouver, je divulgâche ici les trois définitions fondamentales et le théorème qui seront expliquées et commentées dans la suite :

✱ Définition : Si A,P⊆ℕ, un P-questionneur pour A est un couple ⟨m,e⟩ où m et, si u=1A(m) est la valeur de la fonction indicatrice de A en m, alors le programme e appelé sur l'entrée u, termine et renvoie un élément de P.

✱ Définition : Si A,P⊆ℕ, un P-répondeur pour A est un programme qui, quand on lui passe un P-questionneur pour A, termine et renvoie un élément de P.

✱ Définition : Si A,B,P⊆ℕ, un P-convertisseur de B vers A est un programme qui, quand on lui passe un P-répondeur pour B, termine et renvoie un P-répondeur pour A. Et un convertisseur universel de B vers A est un même programme h qui est un P-convertisseur de B vers A pour n'importe quel P⊆ℕ.

✱ Théorème : Pour A,B⊆ℕ, un convertisseur universel de B vers A existe si et seulement si A est Turing-réductible à B.

Je note par ⟨m,n⟩ un codage (calculable, évidemment) des couples d'entiers naturels par des entiers naturels, et par ⟪k1,…,kr⟫ un codage (calculable) des listes finies d'entiers naturels par des entiers naturels. Les détails de ces codages n'auront pas d'importance. Tant qu'à faire, je noterai k: la liste obtenue en ajoutant k en tête de la liste (c'est-à-dire ⟪k,k1,…,kr⟫ si = ⟪k1,…,kr⟫).

Je suis la convention, habituelle en calculabilité, selon laquelle (via un codage de Gödel) les programmes sont des entiers naturels, prennent un entier naturel en entrée et renvoient un entier naturel (s'ils terminent). Je vais noter en le résultat, s'il est défini, de l'exécution de l'exécution du programme e sur l'entrée n, ce qui se note souvent φe(n) (valeur en n de la e-ième fonction générale récursive φe). On écrit en↓ pour dire que en est défini (i.e., le programme termine).

Inversement, je noterai fun n ↦ (truc), où truc fait intervenir n, le programme qui prend n en entrée et renvoie truc. (Souvent on note ça avec un λ comme en λ-calcul, à savoir λn.(truc), mais ça me semblait vraiment illisible d'utiliser cette notation. Noter qu'en principe, c'est un entier naturel que je définis par cette notation, puisque mes programmes sont représentés comme des entiers naturels.) Par exemple, (fun nn³+1) • 12 = 1729, et donc aussi (fun ee•12) • (fun nn³+1) = 1729.

L'opération d'application ‘•’ s'associe implicitement à gauche : c'est-à-dire que enp doit se comprendre comme (en)•p. Moralement, ici e est une fonction de deux arguments, acceptés sous forme « currifiée » fun nfun p ↦ (truc), c'est-à-dire en prenant d'abord le premier, n, pour renvoyer une fonction prenant le deuxième argument, p et renvoyant le truc final.

Si A⊆ℕ est un ensemble d'entiers naturels, je note 1A sa fonction indicatrice (c'est-à-dire celle qui vaut 1 sur A et 0 ailleurs, ou, informellement, la fonction qui répond à la question mA ?). On dit que A est décidable lorsque 1A est calculable (i.e., lorsqu'il existe d tel que dm = 1A(m) pour tout m∈ℕ).

Si P,Q⊆ℕ sont deux ensembles d'entiers naturels, j'utiliserai occasionnellement la notation PQ pour l'ensemble des e tels que, pour tout nP on ait en↓∈Q (c'est-à-dire que d'une part en est défini, et que d'autre part sa valeur appartient à Q). Informellement, on peut parler de programmes qui envoient P dans Q.

La notation JB(R) sera expliquée plus bas : ce sont les programmes avec B pour oracle qui terminent et renvoient un élément de R.

Pour minimiser la confusion du lecteur, j'ai essayé de suivre la convention de Barendregt selon laquelle la même variable devrait, autant que possible, toujours désigner la même chose : comme il y a plein de lettres qui apparaissent à divers endroits dans la suite, voici une tentative pour rappeler leurs rôles respectifs (les explications suivantes n'ont pas forcément de sens à ce stade, elles en acquerront au fur et à mesure de la suite !). Dramatis personæ, donc :

A
Une partie de ℕ dont on se demande si elle est Turing-réductible à B.
B
Une partie de ℕ qui sera parfois utilisée comme oracle.
c
Un programme prenant en entrée un entier m et une liste de couples ⟨n,v⟩ où n∈ℕ et v=1B(n), et renvoyant soit u=1A(m) soit la demande d'ajouter un nouveau n à la liste.
e
La deuxième partie d'un questionneur pour A : attend il une valeur u=1A(m) (pour renvoyer un bonbon en échange).
η
Programme (fixé) appartenant à RJB(R) pour n'importe quel R⊆ℕ.
f
Un répondeur : il attend qu'on lui fournisse un questionneur (pour renvoyer un bonbon en échange).
g
La deuxième partie d'un questionneur pour B : attend il une valeur v=1B(n) (pour renvoyer un bonbon en échange).
h
Un convertisseur de B vers A : attend un répondeur pour B et en renvoie un pour A.
JB(R)
Programmes avec B pour oracle qui terminent et renvoient un élément de R.
Une liste de couples ⟨n,v⟩ où n∈ℕ et v=1B(n).
m
Un entier naturel dont on se demande s'il appartient à A.
μ
Programme (fixé) appartenant à JB(JB(R)) ⇛ JB(R) pour n'importe quel R⊆ℕ.
n
Un entier naturel dont on se demande s'il appartient à B.
ο
Programme (fixé) appartenant à {n} ⇛ JB({1B(n)}) pour n'importe quel n∈ℕ.
P,Q,R
Des parties de ℕ dont on ne sait rien (les éléments de P seront parfois appelés bonbons).
τ
Programme (fixé) appartenant à (R₁⇛R₂) ⇛ (JB(R₁)⇛JB(R₂)) pour n'importe quels R₁,R₂⊆ℕ.
u
Typiquement la réponse 1A(m) à la question mA ?.
v
Typiquement la réponse 1B(n) à la question nB ?.

J'ai utilisé quelques autres notations dans les bouts de pseudocode qui devraient être assez évidentes : notamment case … of pour faire du pattern-matching, universal_interpreter pour un interpréteur universel (i.e., universal_interpreteren vaut en par définition) et universal_oracle_interpreter pour la même chose pour une machine avec oracle, et call_oracle pour l'appel à l'oracle dans une telle machine (donc call_oracle appelé sur n renvoie, disons, 1B(n)). Et j'utilise des marqueurs comme 'found et 'notfound ou 'final et 'moreq juste pour marquer des distinctions de cas (on peut supposer que ce sont des entiers naturels arbitraires mais distincts ; et avant que quelqu'un n'ergote au sujet du fait que j'ai écrit ⟨'notfound⟩ tout seul, mettons que c'est une abréviation de ⟨'notfound, 0⟩).

La réduction de Turing (une brève présentation)

Si A,B⊆ℕ sont deux ensembles d'entiers naturels[#5], la définition habituelle de la réduction de Turing (que j'avais tenté de vulgariser ici) est quelque chose comme ceci : on dit que A est Turing-réductible à B lorsqu'il existe un programme qui prend en entrée un entier m∈ℕ, termine en temps fini et décide si mA (i.e., répond oui (1) si c'est le cas et non (0) si mA), sachant que ce programme a la capacité « magique », en plus de ce que peut faire ordinairement un programme (disons, une machine de Turing), d'interroger un oracle qui teste l'appartenance à B (i.e., on présente à l'oracle un entier n∈ℕ, et il répond — immédiatement — oui (1) si nB et non (0) si nB). Intuitivement, donc, ça traduit le fait que si je donne (« magiquement ») à un ordinateur la capacité de répondre à la question est-ce que ce truc appartient à B ? (sans limite sur le nombre de questions posées ou sur les trucs sur lesquels on les pose, il faut juste terminer en temps fini), on peut alors répondre à la question est-ce que ce machin appartient à A ?. Encore plus intuitivement, B est au moins aussi difficile à calculer que A.

[#5] Le fait que je fasse la définition pour des parties A,B⊆ℕ (i.e., sur des « problèmes de décision ») plutôt que des fonctions ℕ→ℕ n'a pas d'importance dans ce contexte : la réduction de Turing se définit de façon tout aussi standard sur les fonctions (si je donne magiquement à un ordinateur la capacité de calculer l'une, alors ça lui permet de calculer l'autre). Je vais revenir là-dessus à la fin, mais pour l'instant c'est plus commode de travailler avec des parties.

Une partie énorme de la théorie de la calculabilité consiste à étudier, sous une forme ou une autre, parfois avec des variantes, cette notion de réduction de Turing (ainsi que les degrés de Turing, qui sont les classes d'équivalence de la relation chacun de ces deux ensembles est Turing-réductible à l'autre, appelée équivalence de Turing). En tout cas, c'est une notion de la plus haute importance.

Néanmoins, on peut trouver cette définition un peu désagréable : une fois qu'on a défini la calculabilité de Church-Turing, on aimerait bien oublier la définition, et travailler uniquement sur la notion de fonction calculable indépendamment de sa définition (surtout qu'il y en a plusieurs). Mais voilà que la définition de la réduction de Turing nous oblige à « rouvrir » la définition, pour en introduire une variante (à savoir : la calculabilité avec oracle) : voilà qu'on nous dit ah, en fait, tout le travail qu'on a fait sur les machines de Turing, pour définir le concept et en démontrer les propriétés élémentaires, ben il faut le refaire pour les machines de Turing avec oracle, mais ne vous inquiétez pas, c'est tout pareil, on va laisser en exercice au lecteur de vérifier les détails. Un peu agaçant.

On peut donc légitimement se demander : supposons que je ne veuille absolument pas « rouvrir » la définition de la calculabilité, est-ce que je peux quand même définir la réduction de Turing ? Disons, trouver une notion qui lui est équivalente ?

Alors une façon de faire est la suivante[#6] : on dit que A est Turing-réductible à B lorsqu'il existe un programme (au sens usuel ! c'est-à-dire, sans oracle) qui prend en entrée une question mA ? et une liste (finie) de réponses connues à des questions nB ? et doit soit donner une réponse définitive à la question mA ? soit demander à ajouter une nouvelle question à la liste, et de plus, si on ajoute de façon répétée la réponse correcte aux questions qu'il pose, le processus doit terminer et finit par donner la réponse correcte à la question mA ? qu'on lui a posée. De façon plus formelle (et très laborieuse !) : on dit que A est Turing-réductible à B lorsqu'il existe un programme c qui, quand on lui fournit en entrée un entier m et une liste ⟪⟨n1,v1⟩, …, ⟨nr,vr⟩⟫ de couples ⟨ni,vi⟩ où à chaque fois vi = 1B(ni) est la valeur de la fonction indicatrice de B en ni (i.e., la réponse à la question est-ce que ni est dans B), va soit renvoyer ⟨'final, u⟩ où u = 1A(m), soit renvoyer ⟨'moreq, n⟩ ; et de plus, si on appelle c de façon répétée sur le même m, en commençant avec la liste vide, et en ajoutant ⟨n,v⟩ où v = 1B(n) à la liste à chaque fois qu'il renvoie ⟨'moreq, n⟩, alors au bout d'un nombre fini d'itérations il finit par renvoyer ⟨'final, u⟩ où u = 1A(m). Mais pfiou, c'est assez fastidieux à écrire, et en fait c'est un mince déguisement de la définition basée sur des machines à oracle (essentiellement, on a juste extrait les appels à l'oracle pour les mettre dans une boucle externe).

[#6] Pour ceux qui ont lu ce billet, cette approche consiste essentiellement à donner la stratégie d'Arthur dans le jeu qui y est décrit (on est dans le cas que j'ai appelé T0, où Merlin et Nimué n'ont qu'un seul coup possible [sauf le coup initial où Merlin pose la question en fournissant le m, si on veut], donc c'est un jeu à un seul joueur). Les deux réponses ⟨'final, u⟩ et ⟨'moreq, n⟩ autorisées pour c correspondent aux deux coups possibles d'Arthur : terminer le jeu en déclarant victoire, ou bien proposer une nouvelle valeur à Merlin.

Trois définitions (questionneurs, répondeurs, convertisseurs) et un théorème

Y a-t-il une autre approche possible pour définir la réduction de Turing, donc ? Peut-être quelque chose qui serait plus abstrait ou plus général ? Il semblerait bien que oui, mais en contrepartie c'est peut-être plus délicat à suivre. Je vais essayer de dérouler cette approche en introduisant trois notions successives, que je vais commenter un peu à chaque fois :

✱ Définition : Si A,P⊆ℕ, on appellera P-questionneur pour A (le codage d')un couple ⟨m,e⟩ où m et, si u=1A(m) est la valeur de la fonction indicatrice de A en m, alors le programme e appelé sur l'entrée u, termine et renvoie un élément de P (ce que je peux noter eu↓∈P, où la notation eu désigne la valeur renvoyée par le programme e sur l'entrée u).

Intuitivement, un P-questionneur encode une question est-ce que mA ? et, en même temps, il fournit un programme e auquel on est chargé de fournir[#7] la réponse (u). Encore plus informellement, P est un ensemble de bonbons, le questionneur vous demande est-ce que mA ? et, si vous répondez correctement[#8], il vous donne un bonbon en échange (à savoir eu).

[#7] Si vous avez l'impression ici que e est une continuation, c'est tout à fait l'idée, et je vais y revenir.

[#8] C'est si et pas si et seulement si, car, évidemment, si A n'est pas décidable, le programme e n'a pas les moyens de savoir si vous avez répondu correctement. Donc, pour être bien clair : si vous lui assez autre chose que 1A(m), le programme e a le droit de faire n'importe quoi (vous donner un bonbon, vous donner autre chose qu'un bonbon, ou ne rien vous donner du tout parce qu'il ne termine jamais). La seule contrainte pour être un répondeur, c'est que si u=1A(m) alors eu↓∈P.

Si vous avez lu des choses sur la réalisabilité ou le topos effectif, ce que j'appelle un P-questionneur pour A est (essentiellement la même chose qu')un réalisateur de[#9] ∃m:ℕ.(mA∨¬mAP).

[#9] Pour qu'il n'y ait aucune ambiguïté, l'opération logique ‘∨’ est prioritaire sur ‘⇒’, c'est-à-dire le parenthésage ici est : ∃m:ℕ.((mA∨¬mA) ⇒ P).

L'ensemble P a une importance cruciale ici, évidemment, et il n'est sans doute pas clair à ce stade ce qu'on doit en faire (j'espère que ça s'éclaircira avec la suite). Évidemment, si P=∅ il n'y a pas de ∅-questionneur pour A (quel que soit A), et si P=ℕ il y en a des complètement idiots, par exemple si e est le programme renvoyant toujours 42, alors ⟨m,e⟩ est un ℕ-questionneur pour n'importe quel A, ou d'ailleurs un {42}-questionneur. De façon plus intéressante (et c'est surtout ce type d'exemple qu'on gardera à l'esprit), si e est le programme fun uu qui renvoie immédiatement l'argument qu'on lui passe, alors ⟨m,e⟩ est un {1A(m)}-questionneur pour A, qu'on pourrait qualifier de questionneur évident (pour ce m). Oui, tout ça n'est pas bien passionnant, mais passons à la définition suivante.

✱ Définition : Si A,P⊆ℕ, on appellera P-répondeur pour A un programme qui, quand on lui passe un P-questionneur pour A, termine et renvoie un élément de P. Autrement dit, c'est un f tel que f•⟨m,e⟩↓∈P pour tout P-questionneur pour A.

Intuitivement, un P-répondeur accepte une question est-ce que mA ? et il est « plus ou moins censé » lui fournir la réponse : on « espère vaguement » qu'il va appeler e avec la vraie valeur u=1A(m) pour produire un élément de P et renvoyer cet élément. Mais ce n'est pas demandé : la définition demande juste qu'il renvoie un élément de P quand on lui passe un P-questionneur. Encore plus informellement, le répondeur vous donne un bonbon si vous lui passez un machin qui donne un bonbon si on répond à une certaine question.

Si vous avez lu des choses sur la réalisabilité ou le topos effectif, ce que j'appelle un P-répondeur pour A est (essentiellement la même chose qu')un réalisateur de[#10] ((∃m:ℕ.(mA∨¬mAP)) ⇒ P).

[#10] Avec des parenthèses en plus : ((∃m:ℕ.((mA∨¬mA) ⇒ P)) ⇒ P)

Encore une fois, l'ensemble P a une importance cruciale ici. Par exemple, le programme qui ignore ses entrées et renvoie toujours 42 est ℕ-répondeur pour n'importe quel A, ou d'ailleurs un {42}-répondeur. De façon plus subtile, c'est aussi un ∅-répondeur ! En effet, comme il n'existe pas de ∅-questionneur (quel que soit A), du coup, un ∅-répondeur a la tâche de renvoyer quelque chose d'impossible (un élément de ∅) en échange de quelque chose d'impossible (un ∅-répondeur), et… n'importe quel programme fait ça. Donc n'importe quel programme est un ∅-répondeur pour n'importe quel A ! Du coup, la notion de P-répondeur peut sembler excessivement triviale : s'il y a un élément dans P, je peux renvoyer constamment cet élément, et s'il n'y en a pas, je peux faire n'importe quoi… et je n'ai jamais besoin de consulter A. (Ceci prouve que, quel que soientt les ensembles A et P, il existe toujours un P-répondeur pour A.) Pourtant, on va faire quelque chose avec.

Déjà, pour se préparer à la suite, je peux introduire la notion de répondeur universel pour A : un répondeur universel[#11] pour A est un même programme f qui est un P-répondeur pour A pour n'importe quel P⊆ℕ. Et je souligne que le programme f ne reçoit pas l'information de P (d'ailleurs, on ne sait pas sous quelle forme elle pourrait lui être passée…) : il doit, sans connaître P, être capable de renvoyer un élément de P quand on lui passe un P-questionneur pour A. Et là, les petites astuces idiotes du paragraphe précédent ne marchent plus.

[#11] Si vous avez lu des choses sur la réalisabilité ou le topos effectif, ce que j'appelle un répondeur universel pour A est (essentiellement la même chose qu')un réalisateur de ∀P:Ω. ((∃m:ℕ.(mA∨¬mAP)) ⇒ P).

En fait, il n'est pas difficile de se convaincre de la chose suivante :

✱ Remarque : un répondeur universel pour A existe si et seulement si A est un ensemble décidable (= calculable, = récursif).

(De plus, on va expliciter une façon de transformer algorithmiquement un programme décidant A en un répondeur universel pour A et réciproquement.)

Démonstration : Si A est décidable, mettons que d le décide (au sens où, quel que soit m, on a dm = 1A(m)). Alors je fabrique un répondeur universel pour A de la manière suivante : donné un P-questionneur ⟨m,e⟩, j'appelle simplement e sur la valeur u := dm = 1A(m) et je renvoie cette valeur. (Donc finalement, si on veut, le répondeur annoncé est : funm,e⟩ ↦ e•(dm).) Ceci est bien un P-répondeur, parce qu'on a la garantie que eu↓∈P lorsque u = 1A(m), par le fait que ⟨m,e⟩ est un P-questionneur.

Réciproquement, si f est un répondeur universel, pour décider si mA, j'appelle f sur le questionneur « évident » ⟨m,e⟩ où e est le programme fun uu qui code la fonction identité, et je renvoie la valeur en question. (Donc finalement, si on veut, le décideur annoncé est : fun mf•⟨m, (fun uu)⟩.) Comme ⟨m,e⟩ est un {1A(m)}-questionneur pour A et que f est un répondeur universel, donc notamment un {1A(m)}-répondeur, alors la valeur f•⟨m,e⟩ retournée par f doit être dans {1A(m)}, c'est-à-dire que c'est bien 1A(m). ∎

L'idée est, en quelque sorte, de généraliser cette remarque et sa preuve : d'en obtenir un analogue « relatif » où au lieu de dire que A est décidable on va dire qu'il est décidable relativement à B, i.e., Turing-réductible à B.

Pour ça, on introduit une troisième définition :

✱ Définition : Si A,B,P⊆ℕ, on appellera P-convertisseur de B vers A un programme qui, quand on lui passe un P-répondeur pour B, termine et renvoie un P-répondeur pour A. Et (si A,B⊆ℕ) un convertisseur universel de B vers A est un même programme h qui est un P-convertisseur de B vers A pour n'importe quel P⊆ℕ.

Si vous avez lu des choses sur la réalisabilité ou le topos effectif, ce que j'appelle un P-convertisseur de B vers A est (essentiellement la même chose qu')un réalisateur de ((∃n:ℕ.(nB∨¬nBP)) ⇒ P) ⇒ ((∃m:ℕ.(mA∨¬mAP)) ⇒ P). Et pour un convertisseur universel, bien sûr, c'est la même chose avec P devant la totalité de la formule. (Noter que ce n'est pas pareil que de mettre P devant chacune des deux parties de l'implication, ce qui correspond à la remarque que je vais faire au paragraphe suivant.)

Attention, un convertisseur universel de B vers A est un programme qui convertit un P-répondeur pour B en un P-répondeur pour A pour n'importe quel P pour le même P. Ce n'est pas pareil qu'un programme qui convertit un un répondeur universel pour B en un répondeur universel pour A : cette dernière définition ne serait pas très intéressante puisque, comme je l'ai expliqué plus haut, un répondeur universel pour A n'existe que lorsque A est décidable (donc pour n'importe quelles deux parties non-décidables, il existe un programme qui convertit un un répondeur universel pour B en un répondeur universel pour A tout simplement parce que ce sont deux ensembles vides).

Le théorème qui suit, qui est le centre de ce billet, est la « version relative » promise de la remarque plus haut.

✱ Théorème : Pour A,B⊆ℕ, un convertisseur universel de B vers A existe si et seulement si A est Turing-réductible à B.

(De plus, on va expliciter une façon de transformer algorithmiquement un programme décidant A en utilisant B comme oracle en un convertisseur universel de B vers A et réciproquement.)

D'un programme avec oracle vers un convertisseur universel

Bon, il faut que j'explique les deux sens de l'équivalence affirmée dans mon[#12] théorème.

[#12] Je dis mon théorème parce que je suis en train d'en parler, mais je répète que je n'affirme aucune paternité sur ce théorème, qui est dû à Hyland même is Hyland ne l'a pas affirmé sous cette forme exacte.

Commençons par la transformation d'un programme avec oracle en un convertisseur universel : la situation, donc, est qu'on a un programme avec oracle qui calcule 1A en ayant accès à 1B, et on a aussi un P-répondeur pour B (appelons-le f), pour un certain P non spécifié, et on doit fabriquer un P-répondeur pour A ; ou, ce qui revient au même, on a f un P-répondeur pour B et ⟨m,e⟩ un P-questionneur pour A et on doit fournir un élément de P.

L'idée générale est de transformer le programme avec oracle en continuation-passing-style (CPS). Je vais le redire un peu autrement en-dessous, mais grosso modo, ça signifie qu'on va remplacer chaque appel de fonction censée renvoyer une valeur — en fait, remplacer les appels à l'oracle suffit — par un appel à une fonction qui, au lieu de renvoyer une valeur, prend une « continuation de fait », c'est-à-dire une fonction qui attend cette valeur pour en faire quelque chose. Or la version CPS de l'oracle est exactement ce que nous fournit le répondeur pour B : au lieu prendre n et de de renvoyer la réponse à nB comme le fait un oracle normal, le répondeur f attend un couple ⟨n,g⟩ (un questionneur) où g est une continuation de fait, à qui on va passer cette valeur. Les continuations elles-mêmes renvoient quelque chose de non spécifié, et c'est exactement le rôle que va jouer l'ensemble P dans cette histoire : on ne sait pas ce que c'est, et ça n'a pas d'importance, ça peut être n'importe quoi, l'élément de P renvoyé par l'ensemble du programme est fourni par la continuation finale, qui est ici le e du couple ⟨m,e⟩. Bref : on convertit le programme avec oracle en CPS (ou au moins en mettant en CPS les appels à l'oracle), chaque appel à l'oracle est remplacé par un appel à f avec pour continuation la fonction g qui représente la suite de l'exécution, et comme continuation ultime de tout le calcul on utilise la fonction e fournie par le questionneur.

Si on a trouvé que le paragraphe précédent était vraiment de l'agitage de mains, voici une description plus précise de la transformation. Comme je l'ai dit plus haut, on peut supposer que le programme à transformer, appelons-le c, prend en entrée un entier m et une liste ⟪⟨n1,v1⟩, …, ⟨nr,vr⟩⟫ de couples ⟨ni,vi⟩ où à chaque fois vi = 1B(ni), et il doit soit renvoyer une réponse finale à la question mA ?, soit une demande d'ajouter un nouveau n à la liste, de sorte que si on répond à toutes ses questions correctement, on obtienne la réponse finale correcte en temps fini. On va construire un programme, appelons-le č, qui va prendre une liste comme ci-dessus, f un P-répondeur pour B et ⟨m,e⟩ un P-questionneur pour A, et doit fournir un élément de P. Il (č) procède ainsi : on lance c sur m et la liste  : si c donne une réponse finale u à mA ?, alors on appelle e sur u ; si c demande l'ajout d'un nouveau n, alors on appelle f sur le couple ⟨n,g⟩ où g est la fonction qui prend un v en entrée et appelle récursivement č sur la liste ⟨n,v⟩: et les mêmes f et ⟨m,e⟩ qu'il a reçus. In fine, il n'y a plus qu'à appeler ce č sur la liste vide.

En pseudocode (où je note c•m•ℓ le programme c appelé à m et et ainsi de suite, et je suppose qu'il retourne soit un couple ⟨'final, u⟩ pour fournir une réponse finale u, soit un couple ⟨'moreq, n⟩ pour demander l'ajout d'un n à la liste des questions), c'est quelque chose comme ceci :

let č = fun ℓ ↦ fun f ↦ fun ⟨m,e⟩ ↦
        case c•m•ℓ of
          ⟨'final, u⟩ ↦ e•u
        | ⟨'moreq, n⟩ ↦ f • ⟨n, ( fun v ↦ č•(⟨n,v⟩:ℓ)•f•⟨m,e⟩ )⟩
  in č•⟪⟫

La possibilité d'appeler č dans la définitition de č est justifiée par le théorème de récursion de Kleene. Le convertisseur h final est le programme qui prend c en entrée et renvoie le programme ci-dessus.

La preuve de la correction de ce programme (je rappelle qu'on doit juste montrer que sa valeur de retour est dans P, c'est la seule chose qui est demandée) est une récurrence sur le nombre de questions (appels à l'oracle) que cm va encore poser pour apporter une réponse finale : s'il est nul, alors la valeur de retour de č est eu qui est bien dans P, et s'il est strictement positif, alors (si on a bien v = 1B(n)) l'appel récursif č•(⟨n,v⟩:)•f•⟨m,e⟩ renvoie une valeur dans P par récurrence, donc f appelé là-dessus aussi puisque f est réputé être un répondeur.

D'un convertisseur universel vers un programme avec oracle : une tentative qui échoue

Passons à la transformation d'un convertisseur universel en un programme avec oracle : celle-ci m'a donné beaucoup plus de fil à retordre. Comme ceci est un billet de blog et pas un article de recherche, il est sans doute intéressant que je raconte un peu comment j'ai réfléchi et pourquoi j'ai eu du mal. (Mais on peut sauter directement à la section suivante si on veut juste la preuve du théorème.)

Ce qui rend cette transformation difficile (ou en tout cas, m'a beaucoup embrouillé), c'est : comment utiliser la liberté de choix qu'on sur P ? Comment trouver un P pour lequel on peut utilement trouver un P-répondeur pour B auquel appliquer le convertisseur universel ? (Ce n'est pas évident, parce qu'on a vu que pour tout P il existe toujours un P-répondeur pour n'importe quelle partie !)

Évidemment, ce qu'on aurait envie de faire, c'est de fournir à notre convertisseur h un répondeur qui fait juste un appel à l'oracle, quelque chose comme :

fun m ↦ h • ( fun ⟨n,g⟩ ↦ g • (call_oracle • n) )
           • ⟨m, (fun u ↦ u)⟩

(Ceci est directement censé calculer 1A.) Mais ça ce n'est pas possible, parce que la fonction call_oracle elle n'existe pas. Enfin, elle existe dans un programme avec oracle, mais un répondeur c'est censé être un vrai programme, pas un programme avec oracle : on ne peut pas donner au convertisseur un programme avec oracle en espérant qu'il crache un programme avec oracle. La construction ci-dessus marche effectivement si B est décidable (de sorte qu'on peut implémenter la fonction call_oracle par un vrai programme), mais dans ce cas, de toute façon, on sait que A est décidable donc on n'a rien à prouver (c'est juste redire la remarque faite plus haut).

Ma première idée pour contourner le problème a été de raisonner comme informaticien. Je me suis dit que, comme de toute façon il s'agit de construire un programme qui reçoit des valeurs de 1B dans une liste ′ et soit fournit une réponse finale soit demande à étendre la liste, j'allais utiliser un répondeur pour B qui cherche le n demandé dans la liste : s'il la trouve, il passe la valeur correspondante au questionneur, et sinon, il « soulève une exception », c'est-à-dire qu'il interrompt le flot d'exécution normal (l'appel des continuations) pour demander sur-le-champ une nouvelle valeur. Ici, soulever une exception, ça signifie qu'au lieu d'appeler la continuation à laquelle on est censé fournir le résultat, on renvoie directement un résultat « exceptionnel », que je vais noter ⟨'moreq, n⟩ ici. En pseudocode, ça donne quelque chose comme ceci :

let c = fun m ↦ fun ℓ′ ↦
        h • ( fun ⟨n,g⟩ ↦ case find_in_list • n • ℓ′ of
                             ⟨'found, v⟩ ↦ g•v
                           | ⟨'notfound⟩ ↦ ⟨'moreq, n⟩ )
          • ⟨m, (fun u ↦ ⟨'final, u⟩)⟩

(J'ai supposé que find_in_list • n • ℓ′ renvoie ⟨'found, v⟩ si n est un des ni de la liste ′ =: ⟪⟨n1,v1⟩, …, ⟨nr,vr⟩⟫ et, sinon, renvoie ⟨'notfound⟩.)

Ce que j'essaie de faire, là, donc, c'est que j'appelle mon convertisseur h sur un répondeur pour B (je vais dire dans un instant quel est le P sous-entendu) qui « fait ce qu'il peut » avec le questionneur qu'on lui a fourni : si la question du questionneur est dans la liste ′ qu'il a à sa disposition, alors il fournit la valeur v correspondante au questionneur, et sinon, il interrompt tout en soulevant une exception ⟨'moreq, n⟩. Ensuite, j'appelle le répondeur pour A (que h est censé m'avoir fourni en échange du répondeur pour B que je viens de décrire) sur un questionneur assez évident, sauf que j'encode une vraie réponse sous forme ⟨'final, u⟩ pour distinguer du cas où une exception ⟨'moreq, n⟩ a été soulevée.

L'ensemble P que j'ai en tête (et pour lequel h est appelé sur un P-répondeur pour B et un P-questionneur pour A), ici est l'ensemble formé de ⟨'final, u⟩ où u := 1A(m) est la valeur finale recherchée, mais aussi des ⟨'moreq, n⟩ avec n∈ℕ. Ainsi, si ⟨n,g⟩ est un P-questionneur pour B, et si la liste ′ est remplie de vraies valeurs de 1B, alors aussi bien gv que ⟨'moreq, n⟩ sont des éléments de P, donc mon programme appelle bien h sur un P-répondeur pour B, et il doit ainsi obtenir un P-répondeur pour A d'après le contrat sur le comportement de h.

Et alors, est-ce que ça marche ? Eh bien… peut-être. Je ne sais pas bien.

Si le convertisseur h a été fabriqué comme ci-dessus à partir d'un c (i.e., en le convertissant, en quelque sorte, en continuation-passing-style), alors ça fait bien ce qui était attendu : on retrouve le c de départ (enfin, on retrouve le même comportement que celui-ci).

L'ennui, c'est que rien ne garantit ça : on a juste la garantie que le convertisseur h convertit un P-répondeur pour B en un P-répondeur pour A, pas qu'il a été obtenu à partir de la transformation d'un c par le procédé ci-dessus. Alors, certes, j'ai prouvé ci-dessus que j'avais bien appelé h sur un P-répondeur pour B, donc j'obtiens un P-répondeur pour A, mais… rien ne dit qu'il soit très utile.

À cause de l'ensemble P que j'ai fourni, mon P-répondeur pour A pourrait très bien, pour ce que j'en sais, renvoyer toujours ⟨'moreq, n⟩ quel que soit le questionneur qu'on lui fournit (puisque, par construction, mon ensemble P contient ces valeurs « exceptionnelles » dont j'avais besoin pour faire le répondeur pour B, le répondeur pour A que j'obtiens en retour a bien le droit de les fournir, et rien ne me garantit qu'il ne s'en sert pas abusivement).

Peut-être qu'il y a quand même un argument qui fait que ça marche : je ne sais pas prouver[#13] que la construction que je viens d'écrire ne marche pas, mais je ne sais pas prouver qu'elle marche, et ce serait un chouïa magique si elle marche, mais peut-être en effet qu'il y a moyen de le prouver (par exemple en argumentant que le convertisseur ne peut pas savoir la valeur de moreq et ne peut pas la deviner en inspectant le programme).

[#13] Comme je le disais dans l'introduction, je n'ai pas vraiment compris l'argument de Hyland. Il y a une phrase from the definition of ψ*B, this terminates in a finite number of steps giving DA(n) as required que je ne saisis pas (son ψ*B(P) est ∀Q:Ω. (((∃n:ℕ.(nB∨¬nBQ)) ⇒ Q) ∧ (PQ) ⇒ Q), et DA(m) est mA∨¬mA ou si on veut 1A(m)) : est-ce que l'argument est celui que je donne ci-dessus (qu'il aurait trouvé moyen de faire marcher), ou celui ci-dessous, ou encore autre chose ?

Ce n'est pas grave : dans la section suivante, je vais donner un autre argument, et une autre construction, qui, elle, marche.

D'un convertisseur universel vers un programme avec oracle : une approche qui marche

Revenons à nos moutons, donc. Je veux trouver[#14] comment utiliser un convertisseur universel. Le point crucial est de trouver le bon P pour lequel l'existence d'un P-répondeur pour B soit vraiment une information utile, et auquel appliquer le convertisseur universel.

[#14] Si on se demande comment on trouve une telle démonstration, voici quelques éléments de réponse pour la découvrir ou la décoder. Premièrement, il faut penser à interpréter les oracles comme des topologies de Lawvere-Tierney sur le topos effectif (comme je le dis au paragraphe suivant, je tiens cette idée d'articles de Kihara comme celui-ci ou celui-là). Ensuite, il faut penser que la formule ∀P:Ω. (((∃n:ℕ.(nB∨¬nBP)) ⇒ P) ⇒ ((∃m:ℕ.(mA∨¬mAP)) ⇒ P)) (dont les réalisateurs sont les convertisseurs universels de B vers A), est facilement équivalente à ∀P:Ω. ∀Q:Ω. ((∃m:ℕ.(mA∨¬mAP)) ⇒ (((∃n:ℕ.(nB∨¬nBQ)) ⇒ Q) ∧ (PQ) ⇒ Q)), qui exprime le fait que la plus petite topologie de Lawvere-Tierney qui rend B décidable rend aussi A décidable, pour ça je renvoie à cette question MathOverflow, et notamment le point qui va servir dans ce qui suit est le point (8) de loc. cit. (avec spécifiquement f(P) donné par la formule ∃n:ℕ.(nB∨¬nBP) qui représente les P-questionneurs pour B). Maintenant, il faut réussir à mettre tout ça ensemble sans se tromper, et c'est ce que j'essaie de faire ci-dessous.

Voici une idée fondamentale que je tire des articles de Kihara que j'ai évoqués dans ce billet passé : si P⊆ℕ, je vais appeler JB(P) l'ensemble des programmes avec B comme oracle qui terminent et produisent un résultat dans P (programmes s'entendant ici comme programmes sans entrée : si on n'aime pas ça, mettons qu'ils reçoivent 0 comme entrée). Ceci définit une fonction JB : P ↦ JB(P) de l'ensemble 𝒫(ℕ) des parties de ℕ vers lui-même. Et voici quatre remarques faciles mais essentielles que je dois faire sur cette fonction :

  1. Donné n∈ℕ, je peux algorithmiquement fabriquer un programme avec B comme oracle qui calcule la réponse 1B(n) à la question nB ? (il s'agit essentiellement de renvoyer le programme call_oraclen, qui se fabrique algorithmiquement à partir de n). Je souligne que, si le programme fabriqué a besoin de l'oracle pour s'exécuter, la fabrication du programme (à partir de n), elle, n'a pas besoin d'oracle.

    Ceci fabrique donc un élément de JB({1B(n)}) en fonction de n. Appelons-le, disons, οn.

  2. Si R₁,R₂⊆ℕ, et si j'ai un programme r qui, quand on lui fournit un élément de R₁, termine et renvoie un élément de R₂ (ce que j'ai noté ailleurs comme un élément de R₁⇛R₂), alors je peux algorithmiquement en déduire un programme τr qui, quand on lui fournit un élément de JB(R₁), termine et renvoie un élément de JB(R₂) ; et ceci, sans avoir besoin d'aucune connaissance ni information sur R₁ ni R₂.

    (Avec la notion R₁⇛R pour l'ensemble des programmes qui, quand on fournit un élément de R₁, terminent et renvoient un élément de R₂, je suis en train de dire que j'ai un même élément qui appartient à (R₁⇛R₂) ⇛ (JB(R₁)⇛JB(R₂)) quels que soient R₁,R₂.)

    C'est compliqué à dire, mais plus facile à démontrer : pour fabriquer τr à partir de r il suffit de composer par r un élément de JB(R₁) : en effet, si j'ai un programme avec B comme oracle qui fournit un élément de R₁, alors en le composant par r on obtient un programme avec B comme oracle qui fournit un élément de R₂, et la construction composer un programme avec r est algorithmique (et ne demande pas d'oracle, bien qu'elle manipule des programmes avec oracle !).

    (En pseudocode, mon programme τ est donc quelque chose comme fun r ↦ fun w ↦ compose(r, w).)

  3. Plus facile : si R⊆ℕ, j'ai un programme η qui, quand on lui fournit un élément de R, termine et renvoie un élément de JB(R) ; et ceci, sans avoir besoin d'aucune connaissance ni information sur R.

    (Avec la notion ‘⇛’ introduite ci-dessus, je dis que j'ai un élément qui appartient à R ⇛ JB(R) quel que soit R.)

    C'est évident : donnée une valeur v, je peux algorithmiquement construire le programme qui renvoie simplement v (sans interroger d'oracle, même s'il y a le droit).

  4. Plus délicat : si R⊆ℕ, j'ai un programme μ qui, quand on lui fournit un élément de JB(JB(R)), termine et renvoie un élément de JB(R) ; et ceci, sans avoir besoin d'aucune connaissance ni information sur R.

    (Avec la notion ‘⇛’ introduite ci-dessus, je dis que j'ai un élément qui appartient à JB(JB(R)) ⇛ JB(R) quel que soit R.)

    Ici, je suppose que j'ai un programme (avec oracle !) qui renvoie un programme (avec oracle !) qui renvoie un élément de R, appelons-le w (élément de JB(JB(R))) et je dois le convertir (sans oracle !) en un programme (avec oracle !) qui renvoie un élément de R. Il s'agit d'exécuter w, puis d'exécuter le résultat renvoyé par w, et de fournir le résultat de ça : toutes ces exécutions ont besoin de l'oracle, mais la conversion entre le programme w et le programme qui exécute w puis exécute son résultat, elle, n'a pas besoin d'oracle, elle a juste besoin de la possibilité d'écrire une machine universelle.

    (En pseudocode, mon programme μ est quelque chose comme fun w ↦ compose(universal_oracle_interpreter, w).)

Bon, et maintenant que j'ai fait toutes ces remarques[#15], quel est le rapport avec le schmilblick ?

[#15] Si on cherche à réinterpréter (1)–(3), les mathématiciens pourront penser que j'ai expliqué ici que JB est une topologie de Lawvere-Tierney sur le topos effectif. Mais ici, on peut peut-être préférer penser à la notion de monade (ici sur la catégorie des parties de ℕ avec les fonctions calculables comme morphismes) : pour les mathématiciens, η et μ sont les notations habituelles pour l'unité et la multiplication d'une monade (et mon τ est l'action du foncteur de la monade elle-même), mais si je dois parler à un programmeur Haskell, je dirai que les programmes avec B comme oracle et renvoyant R forment un type qui est une monade de R, et ce que j'ai noté η est le return de cette monade, mon τ est fun r ↦ fun w ↦ w >>= (return ∘ r) ou de façon équivalente fun r ↦ fun w ↦ do { x ↤ w ; return (r x) } si on me pardonne ce gloubi-boulga entre les notations de Haskell et les miennes, et mon μ est fun w ↦ w >>= (fun x ↦ x) ou de façon équivalente fun r ↦ fun w ↦ do { x ↤ w ; x }. J'avoue cependant que l'apparition de la notion de monade ici me laisse encore perplexe et que je ne sais pas quel sens profond lui donner.

Mon but est de trouver un P et un P-répondeur pour B qui soit « intéressant », auquel je puisse appliquer le convertisseur universel. Et je vais prendre P = JB(R) (pour un R qui reste à déterminer, mais ce ne sera pas ça qui sera compliqué). Comment est-ce que ça fonctionne ?

Si P⊆ℕ et que ⟨n,g⟩ est un P-questionneur pour B, alors par définition exécuter g sur 1B(n) renvoie un résultat dans P. Comme on peut facilement fabriquer un programme avec oracle qui renvoie 1B(n) (c'est la remarque (0) ci-desus, où j'ai noté οn ce programme), on peut aussi en fabriquer un qui renvoie le résultat de g appelé sur 1B(n) (c'est la remarque (1) ci-dessus, et du coup le programme en question est (τg)•(οn)) ; encore une fois, je parle juste de fabriquer le programme en fonction de n, pas de l'exécuter (l'exécution a besoin de l'oracle, mais pas la fabrication du programme). Bref, ceci nous donne, pour n'importe quel P⊆ℕ (qu'il n'est pas besoin de connaître !) et pour ⟨n,g⟩ n'importe quel P-questionneur pour B, un élément (τg)•(οn) de JB(P).

Appliquons ce qui vient d'être dit au cas particulier P := JB(R) (où R⊆ℕ est, pour l'instant, quelconque). Alors, pour ⟨n,g⟩ n'importe quel JB(R)-questionneur pour B, l'élément (τg)•(οn) est dans JB(JB(R)). Par conséquent, en appliquant la remarque (3) ci-dessus, μ•((τg)•(οn)) est dans JB(R).

Mais ce qu'on vient de montrer là, c'est qu'on a fabriqué un JB(R)-répondeur pour B (à savoir funn,g⟩ ↦ μ•((τg)•(οn))), puisqu'on vient de voir qu'il renvoie un élément de JB(R) quel que soit R⊆ℕ et quel que soit le JB(R)-questionneur pour B. Je peux donc lui appliquer le convertisseur universel, et j'obtiens un JB(R)-répondeur pour A (à savoir h • (funn,g⟩ ↦ μ•((τg)•(οn)))).

C'est presque bon : il n'y plus qu'à trouver un questionneur auquel appliquer ça. Or ce n'est pas difficile : d'après la remarque (2) ci-dessus, ⟨m,η⟩ est un JB({1A(m)})-répondeur pour A. Donc en appliquant le répondeur qu'on vient de dire à ce questionneur, on a un élément de JB({1A(m)}), précisément

h • (fun ⟨n,g⟩ ↦ μ•((τ•g)•(ο•n)))
    ⟨m,η⟩

— et c'est bien ce qu'on voulait, puisqu'un élément de JB({1A(m)}) c'est un programme avec B pour oracle qui répond à la question mA ? et qu'on l'a fabriqué de façon algorithmique[#16] en fonction de m.

[#16] On peut protester que la mission était de fournir un seul et même programme (pour h donné) qui, en disposant de B pour oracle, calcule 1A(m) en fonction de m. Mais c'est facile de régler ce problème : il s'agit juste d'ajouter un peu de sauce au Curry : fun m ↦ universal_oracle_interpreter • truc, où truc est remplacé par ce qui précède, est un programme avec B pour oracle qui calcule 1A (en commençant par calculer le programme truc qui calcule 1A(m) et en l'exécutant ensuite).

Alors oui, certes, c'est assez illisible, et je ne suis toujours pas sûr d'avoir bien compris ce qui s'est passé, mais ceci conclut la preuve du théorème : on a (algorithmiquement !) transformé un convertisseur universel en un programme avec oracle.

(Il serait intéressant de vérifier que les deux transformations que j'ai expliquées sont, en un certain sens qu'il s'agirait de définir, essentiellement inverses l'une de l'autre. Là non plus, je n'ai pas les idées aussi claires que je voudrais.)

Des possibilités de généralisation ?

Il y a encore pas mal de choses que je ne comprends pas bien, mais ceci ne doit pas empêcher de réfléchir à la possibilité de généraliser (comme je l'ai signalé dans ce billet passé, généraliser peut aider à mieux comprendre).

La première remarque est que j'ai utilisé des parties A,B⊆ℕ, qui tiennent en fait lieu de leurs fonctions indicatrices 1A,1B, mais ça n'a joué aucun rôle ici, et je pouvais faire exactement le même raisonnement pour la réduction de Turing d'une fonction α à une autre β. Voici les définitions modifiées[#17] :

  • un P-questionneur pour α est un couple ⟨m,e⟩ où m et, si u=α(m) est la valeur de la fonction α en m, alors le programme e appelé sur l'entrée u, termine et renvoie un élément de P ;
  • un P-répondeur pour α sera un programme qui, quand on lui passe un P-questionneur pour α, termine et renvoie un élément de P ;
  • un P-convertisseur de β vers α sera un programme qui, quand on lui passe un P-répondeur pour β, termine et renvoie un P-répondeur pour α ; et un convertisseur universel de β vers α sera un même programme qui est un P-convertisseur de β vers α quel que soit P.

Alors le théorème est qu'il existe un convertisseur universel de β vers α existe si et seulement si α est Turing-réductible à β (et de plus, on peut transformer, etc.).

[#17] Si vous avez lu des choses sur la réalisabilité ou le topos effectif, ce que j'appelle un P-questionneur pour α est (essentiellement la même chose qu')un réalisateur de ∃m:ℕ.((∃u:ℕ.⟨m,u⟩∈α) ⇒ P), et on n'aura pas de mal à convertir les autres. Donc l'analogue de la partie A est décidable est joué par la fonction α est totale.

Mais ceci suggère à son tour les généralisations suivantes :

  1. Et si on permet aux fonctions α,β de ne plus être totales ?

    Un P-questionneur pour une fonction α qui n'est plus nécessairement totale sera un couple ⟨m,e⟩ où m doit être dans le domaine de définition de α, et le reste est identique.

  2. Et si on permet aux fonctions α,β de prendre un ensemble quelconque de valeurs ? I.e., ce sont maintenant des fonctions partielles de ℕ vers 𝒫(ℕ) ; il faut y penser comme une forme de non-déterminisme.

    Un P-questionneur pour une telle fonction α sera un couple ⟨m,e⟩ où m doit être dans le domaine de définition de α, si uα(m) est une valeur quelconque de la fonction α en m, alors le programme e appelé sur l'entrée u, termine et renvoie un élément de P. (Le reste est identique.)

  3. Et si on permet aux fonctions α,β de prendre une « entrée secrète » ? Autrement dit, ce sont maintenant des fonctions partielles de ℕ×Λ vers 𝒫(ℕ), où Λ est un certain ensemble non spécifié. Ou bien, si on n'aime pas l'idée d'avoir un ensemble non spécifié qui traîne dans l'histoire, des fonctions (totales) de ℕ vers 𝒫(𝒫(ℕ)), cette dernière étant à la fonction partielle α : ℕ×Λ ⇢ 𝒫(ℕ) la fonction ℕ → 𝒫(𝒫(ℕ)) qui à m associe l'ensemble des valeurs Ξ = α(m,ξ) qui sont définies où ξ parcourt Λ. (Il faut y penser à ces fonctions comme une forme de co-non-déterminisme.)

    Un P-questionneur pour une telle fonction α : ℕ×Λ ⇢ 𝒫(ℕ) sera un couple ⟨m,e⟩ où il existe un ξΛ tel que α(m,ξ) soit défini et quel que soit uα(m,ξ), le programme e appelé sur l'entrée u, termine et renvoie un élément de P.

    Si on préfère la présentation comme α : ℕ → 𝒫(𝒫(ℕ)), un P-questionneur pour une telle fonction α sera un couple ⟨m,e⟩ où il existe un Ξα(m) tel que pour tout uΞ, le programme e appelé sur l'entrée u, termine et renvoie un élément de P.

    Dans tous les cas, la notion de P-répondeur et de convertisseur reste inchangée (un P-répondeur est un programme qui prend en entrée un P-questionneur et renvoie un élément de P).

    (Si on a du mal avec ce second cas, on pourra réfléchir à l'exemple de la fonction Error1/k, pour k≥2, qui, vue comme une fonction ℕ → 𝒫(𝒫(ℕ)), est la fonction constante dont la valeur est l'ensemble des parties à k−1 éléments de {0,…,k−1} : un P-questionneur pour cette fonction est essentiellement — on peut ignorer le m qui ne sert à rien — une programme e qui, pour (au moins !) k−1 des k éléments i de {0,…,k−1}, termine quand on l'appelle sur i et renvoie un élément de P.)

Sauf erreur de ma part, la notion de réduction présentée par l'existence d'un convertisseur universel dans chacun de ces cas donne naissance exactement à la théorie des degrés que j'avais appelés T1, T2 et T3 dans ce billet. Normalement, on devrait pouvoir dérouler l'équivalence entre la présentation que je viens de donner et celle qui était donnée dans le billet en question au moyen d'un jeu à trois joueurs entre Arthur, Merlin et Nimué. (Autrement dit, normalement, l'existence d'un convertisseur universel est équivalente à l'existence d'une stratégie gagnante pour Arthur dans le jeu qui est décrit dans ce billet.) On va dire que, euh, je laisse ça en exercice au lecteur. (Bon, si on veut juste vérifier qu'on a bien compris les définitions, on devrait pouvoir se convaincre de l'existence d'un convertisseur universel de Error½ vers A pour n'importe quel A⊆ℕ, ce qui est censé être essentiellement trivial.)

Ensuite, ce qui est intéressant, et comme je l'ai suggéré dans l'introduction, c'est que le point de vue exposé ici a un sens dans un contexte beaucoup plus large (la formule logique ∀P:Ω. (((∃n:ℕ.(nB∨¬nBP)) ⇒ P) ⇒ ((∃m:ℕ.(mA∨¬mAP)) ⇒ P)), ou plus généralement ∀P:Ω. (((∃y:Y.(DB(y) ⇒ P)) ⇒ P) ⇒ ((∃x:X.(DA(x) ⇒ P)) ⇒ P)), a un sens dès qu'on se donne des parties A,B de ℕ, ou plus généralement des formules DA,DB d'objets X,Y, dans un topos quelconque ; et elle traduit le fait que la plus petite topologie de Lawvere-Tierney qui rend B décidable rend aussi A décidable, ou plus généralement qui rend DB vrai rend aussi DA vrai). Ceci suggère donc de regarder comment on peut interpréter cette formule dans toutes sortes de contextes[#18], et si on peut développer une théorie de la réduction de Turing « synthétique » qui utilise simplement cette formule comme fondement.

[#18] Je pense par exemple au topos de la réalisabilité fonctionnelle (c'est-à-dire celui basé sur la seconde algèbre de Kleene comme le topos effectif et la calculabilité usuelle l'est à la première ; donc en gros, ça reviendrait à remplacer des fonctions calculables ℕ→ℕ par des fonctions continues ℕ → ℕ dans tout ce que j'ai raconté), au topos de Kleene-Vesley, au topos de la réalisabilité extensionnelle (cf. ici). Mais on peut même interpréter la formule dans un topos de faisceaux sur un espace topologique (ou une locale) : elle signifie alors que A est décidable sur la plus grande sous-locale sur laquelle B est décidable, ce qui est indiscutablement une condition assez naturelle et intéressante.

Voilà, mes pensées sur toutes ces questions sont encore largement en cours, mais le fait d'écrire ce billet m'aura permis de les éclaircir considérablement, et j'espère pas trop aux dépens de maux de têtes de mon lectorat.

↑Entry #2819 [older| permalink|newer] / ↑Entrée #2819 [précédente| permalien|suivante] ↑

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]