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
- Plan
- Introduction non technique (pourquoi ce billet ?)
- Quelques notations et conventions
- La réduction de Turing (une brève présentation)
- Trois définitions (questionneurs, répondeurs, convertisseurs) et un théorème
- D'un programme avec oracle vers un convertisseur universel
- D'un convertisseur universel vers un programme avec oracle : une tentative qui échoue
- D'un convertisseur universel vers un programme avec oracle : une approche qui marche
- Des possibilités de généralisation ?
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:ℕ.(n∈B∨¬n∈B
⇒ P)) ⇒ P) ⇒
((∃m:ℕ.(m∈A∨¬m∈A
⇒ P)) ⇒ 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 n∈B∨¬n∈B
et m∈A∨¬m∈A 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 e•n 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 e•n↓ pour dire que e•n 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
n
↦ n³+1) • 12 = 1729, et donc aussi
(fun
e ↦ e•12) •
(fun
n ↦ n³+1) = 1729.
L'opération d'application ‘•’ s'associe implicitement à gauche :
c'est-à-dire que e•n•p doit se
comprendre comme (e•n)•p.
Moralement, ici e est une fonction de deux arguments,
acceptés sous forme « currifiée » fun
n
↦ fun
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 m∈A ?
). On dit que A
est décidable
lorsque 1A est
calculable (i.e., lorsqu'il existe d tel
que d•m
= 1A(m) pour
tout m∈ℕ).
Si P,Q⊆ℕ sont deux ensembles d'entiers
naturels, j'utiliserai occasionnellement la
notation P⇛Q pour l'ensemble des e
tels que, pour tout n∈P on
ait e•n↓∈Q (c'est-à-dire que d'une
part e•n 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 à R ⇛ JB(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
m∈A ?
. - v
- Typiquement la
réponse 1B(n) à la
question
n∈B ?
.
J'ai utilisé quelques autres notations dans les bouts de pseudocode
qui devraient être assez évidentes : notamment
pour faire du
pattern-matching, case …
of
pour un
interpréteur universel (i.e., universal_interpreter
universal_interpreter
• e • n vaut e • n par
définition) et
pour
la même chose pour une machine avec oracle,
et universal_oracle_interpreter
pour l'appel à l'oracle dans une
telle machine (donc call_oracle
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 m∈A (i.e.,
répond oui
(1) si c'est le cas et non
(0)
si m∉A), 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 n∈B
et non
(0) si n∉B). 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
. Un peu
agaçant.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
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 m∈A ?
et une liste
(finie) de réponses connues à des
questions n∈B ?
et doit soit donner une
réponse définitive à la question m∈A ?
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 m∈A ?
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 e•u↓∈P, où la
notation e•u
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 m∈A ?
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 m∈A ?
et, si vous répondez
correctement[#8], il vous donne
un bonbon en échange (à savoir e•u).
[#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 e•u↓∈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:ℕ.(m∈A∨¬m∈A ⇒ P).
[#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:ℕ.((m∈A∨¬m∈A) ⇒ 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
u ↦ u 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 m∈A ?
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:ℕ.(m∈A∨¬m∈A ⇒ P)) ⇒ P).
[#10] Avec des parenthèses en plus : ((∃m:ℕ.((m∈A∨¬m∈A) ⇒ 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:ℕ.(m∈A∨¬m∈A ⇒ P)) ⇒ 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 d•m = 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 := d•m = 1A(m) et je renvoie cette valeur. (Donc finalement, si on veut, le répondeur annoncé est :
fun
⟨m,e⟩ ↦ e•(d•m).) Ceci est bien un P-répondeur, parce qu'on a la garantie que e•u↓∈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 m∈A, j'appelle f sur le questionneur « évident » ⟨m,e⟩ où e est le programme
fun
u ↦ u qui code la fonction identité, et je renvoie la valeur en question. (Donc finalement, si on veut, le décideur annoncé est :fun
m ↦ f•⟨m, (fun
u ↦ u)⟩.) 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:ℕ.(n∈B∨¬n∈B
⇒ P)) ⇒ P) ⇒
((∃m:ℕ.(m∈A∨¬m∈A
⇒ P)) ⇒ 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 à n∈B 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 m∈A ?
, 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 à m∈A ?
, 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
le
programme c appelé à m et ℓ et ainsi
de suite, et je suppose qu'il retourne soit un couple c•m•ℓ
⟨'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 c•m•ℓ va encore poser pour apporter une réponse finale : s'il est nul, alors la valeur de retour de č est e•u 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 g•v 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:ℕ.(n∈B∨¬n∈B
⇒ Q)) ⇒ Q) ∧ (P ⇒ Q)
⇒ Q), et DA(m)
est m∈A∨¬m∈A 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:ℕ.(n∈B∨¬n∈B ⇒ P)) ⇒ P) ⇒ ((∃m:ℕ.(m∈A∨¬m∈A ⇒ P)) ⇒ P)) (dont les réalisateurs sont les convertisseurs universels de B vers A), est facilement équivalente à ∀P:Ω. ∀Q:Ω. ((∃m:ℕ.(m∈A∨¬m∈A ⇒ P)) ⇒ (((∃n:ℕ.(n∈B∨¬n∈B ⇒ Q)) ⇒ Q) ∧ (P ⇒ Q) ⇒ 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:ℕ.(n∈B∨¬n∈B ⇒ P) 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 :
-
Donné n∈ℕ, je peux algorithmiquement fabriquer un programme avec B comme oracle qui calcule la réponse 1B(n) à la question
n∈B ?
(il s'agit essentiellement de renvoyer le programme
, 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.call_oracle
• nCeci fabrique donc un élément de JB({1B(n)}) en fonction de n. Appelons-le, disons, ο•n.
-
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)
.) -
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).
-
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 fun
⟨n,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 • (fun
⟨n,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 m∈A ?
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 :
-
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.
-
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.)
-
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
Error
1/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:ℕ.(n∈B∨¬n∈B ⇒ P)) ⇒ P) ⇒ ((∃m:ℕ.(m∈A∨¬m∈A ⇒ P)) ⇒ 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.