Comments on Un regard alternatif sur la réduction de Turing

@Informatheux, @Ruxor : C'est là que je me dis que j'aurais dû écrire mes commentaires ici plutôt que sur Bluesky, pour que la discussion soit centralisée. Manifestement, Ruxor a été dirigé vers ce papier d'Andrew Swan indépendamment par toi ici, par Naïm Favier sur Twitter et par moi sur Bluesky 🙃

Il y a une théorie de la calculabilité synthétique qui gère les degrés de Turing de façon abstraite, ou en tout cas, un début de théorie. Je ne sais pas trop ce qu'il en est, mais j'ai un ami qui m'a expliqué hier son travail de stage avec Andrew Swan (je prétends pas avoir tout compris), qui a travaillé sur les modalités d'oracle dans les ensembles cubiques (<URL: https://arxiv.org/abs/2406.05818) >. Son travail de stage, c'était d'étendre la modalité "oracle pour la fonction f" (qui est paramétrée par la famille de type "f(n) termine") à des familles de (n-)types plus générales (les CW-complexes finis), et comment cette notion généralise la notion d'ensembles récursivement énumérables.

@jeanas

Oui, c'est une bonne remarque. C'est une version plus forte de mon “il y a trop de réaliseurs”. Mais c'est une faiblesse plus pernicieuse du modèle de réalisabilité. Probablement plus intéressante aussi. On ne peut pas la régler avec le λ-calcul comme je proposais plus bas. Je le formulerais comme: la réalisabilité ne sait pas distinguer un ensemble qui doit être vide, d'un ensemble vide juste parce qu'on n'a pas assez de termes dans le langage des réaliseurs.

Je trouve ça un peu frustrant. La seule solution que je vois c'est de faire de la réalisibilité dans des préfaisceaux (aka modèles de Kripke), où on pourrait imaginer que tous les types habitables ont un monde où ils sont non-vides. Mais ce n'est pas très satisfaisant (j'ai l'intuition, cela dit, que ça a un rapport avec les effets, donc ce n'est pas forcément une solution fondamentalement différente du continuation-passing). Après on a besoin de tels modèles pour la logique linéaire, alors ce n'est pas forcément super grave. Mais bon, à ce stade, je pense juste à voix haute, désolé.

@Arnaud Spiwack :

Dès que B est indécidable, il n'y a aucun réalisateur de (∀n∈ℕ. n∈B∨¬n∈B), donc *tous* les entiers sont des réalisateurs de (∀n∈ℕ. n∈B∨¬n∈B)→(∀n∈ℕ. n∈A∨¬n∈A) (un entier réalise ça si vu comme programme il renvoie un décideur de A lorsqu'on lui passe un élément de l'ensemble vide : la condition est « vacuously true »).

Tout ça m'inspire quelques pensées.

En premier, l'idée générale c'est qu'un décideur de A avec oracle de B, finalement, c'est un réalisateur de (∀n∈ℕ. n∈B∨¬n∈B)→(∀n∈ℕ. n∈A∨¬n∈A)

SAUF QUE.

Sauf qu'il y a trop de tels réaliseurs, parce qu'ils ont le droit de regarder comment l'oracle est défini (par exemple, si il est plus grand que 57). C'est pas bien, c'est trop intentionnel et ça va probablement créer tout un tas de programme.

Et c'est le rôle que va jouer le P universellement quantifié: t'empêcher de regarder la valeur de l'oracle. Ça élimine des programmes indésirables. Si on est en λ-calcul et que les réaliseurs sont des termes pas des codes pour des termes, alors il me semble que (∀n∈ℕ. n∈B∨¬n∈B)→(∀n∈ℕ. n∈A∨¬n∈A) et ∀P. (∀n∈ℕ. ((n∈B∨¬n∈B)→P)→P)→(∀n∈ℕ. ((n∈A∨¬n∈A)→P)→P) sont équivalent

(je mets des arguments de type avec @, comme en Haskell, pour la lisibilité; les arguments avec des prime sont des continuations, seconde prennent des continuations en argument)

Forward: λ f @P o'' n a'. o'' n (a' ∘ f))
Backward: λ f'' o n. f'' @(n∈A∨¬n∈A) (λm b'. b' (o m)) n (λx.x)

Une fois muni de tout ça, on peut dire que, du coup, mon réaliseur de ∀P. (∀n∈ℕ. ((n∈B∨¬n∈B)→P)→P)→(∀n∈ℕ. ((n∈A∨¬n∈A)→P)→P) est aussi moralement un réaliseur de la même formule en calculabilité sous oracle. Puis on fait backward, puis on applique à l'oracle, puisqu'on en a un maintenant.

---

Deuxième pensée: les monades.

Ok, donc les monades, c'est utilisé pour modéliser les effets. C'est-à-dire le calcul qui n'est pas purement algorithmique. On pense souvent aux exceptions et à un état mutable. Mais interroger quelqu'un hors du modèle de calcul (Gro-Tsen, Merlin, ou… un oracle), c'est aussi un effet.

Donc une autre façon de penser notre problème, c'est: soit une fonction qui décide B, mais en faisant potentiellement un effet, alors je peux décider A (avec le même effet. Donc, pour une monade T:

T (∀n∈ℕ. n∈B∨¬n∈B) → T (∀n∈ℕ. n∈A∨¬n∈A)

Mais bon, c'est un peu pénible d'avoir à introduire des monades dans la logique pour ça. Ça complique pas mal les choses. Il se trouve, néanmoins, que la monade de continuation est la plus générale des monades (e.g. http://blog.sigfpe.com/2008/12/mother-of-all-monads.html ).

Donc on dit, ok, il y a un P tel que

(∀n∈ℕ. ((n∈B∨¬n∈B)→P)→P)→(∀n∈ℕ. ((n∈A∨¬n∈A)→P)→P)

Puis on dit que c'est pour tout P pour dire qu'on n'utilise pas nous-même d'effet (c'est une fonction pure, aka algorithmique), ou, de manière équivalente, qu'on peut être utilisé quel que soit l'effet ambiant.

---

Tout ça, ce n'est pas des preuves, mais je pense que ça peut être rendu précis.