Comments on La réalisabilité propositionnelle, et ce qu'elle nous apprend sur les algorithmes

[Pour résumer, j'ai l'impression que la réalisabilité propositionnelle se rapproche des réductions non-boîte-noire en algo/complexité/calculabilité (je ne sais pas vraiment s'il y a des applications dans le dernier cas, hors précisément celui de la R.P. mais ce serait tricher ?), tandis que la correspondance C.-H. est typiquement boîte-noire.]

Je suis en train de relire cette entrée (en faisant les exercices, cette fois (ouf, j'ai réussi celui qui est "vraiment facile")), et je me suis fait la réflexion suivante (qui ne va peut-être pas très loin, mais qui ne me semble pas non plus complètement dénuée d'intérêt ?) :

Une des raisons pour lesquelles la R.P. permet de prouver plus de choses que la C.C.-H. (intuitionniste), c'est qu'elle peut recourir à l'exécution entrelacée ; ceci nécessite de connaître "complètement" les programmes à entrelacer (dans un certain modèle de calcul), et ne se contente pas de juste pouvoir les appeler comme boîte noire (ce qui est nécessaire et suffisant (?) avec la C.C.-H., à partir du moment où ils ont le bon type).

Ceci me fait penser à la distinction entre réduction boîte-noire (le type habituel de réduction) et non-boîte-noire (cf. ci-dessous pour quelques exemples) : dans le premier cas (qui se rapproche de la C.C.-H.), on base la réduction sur un oracle (qui respecte des spécifications données par la réduction), tandis que dans le second (qui se rapproche de la R.P.) on a besoin de la donnée d'un programme (dans un certain modèle de calcul, donné par la réduction), (qui à nouveau respecte certaines spécifications données par la réduction). Or le second type de réduction permet effectivement dans certains cas de produire des réductions qui coûtent moins cher que dans le premier (et possiblement n'existent même pas ?).

Bref, je ne sais pas si on peut pousser plus loin cette analogie (par exemple, est-ce qu'on a tout dit en disant que C.C.-H. (intuitionniste) c'est boîte-noire + correction totale, et R.P. c'est non-boîte-noire + correction partielle ??), mais comme j'aime bien le concept de réduction non-boîte-noire je suis toujours content de le recaser :P

## Deux exemples classiques de réductions non-boîte-noires (formulés informellement, et peut-être un peu faux tels que présentés ?). (Dans les deux cas, le programme utilisé par la réduction doit être un circuit (ou un straight-line program, ce qui est la même chose), mais ce n'est pas une règle générale (je pense)) :

- Principe de transposition : si j'ai un circuit qui calcule une application linéaire, alors je peux en déduire un circuit qui calcule sa transposée, et qui a le même coût que le premier.

- Différentiation automatique / backpropagation etc. : si j'ai un circuit qui calcule une fonction, je peux en déduire un circuit qui évalue toutes ses dérivées partielles, pour le même coût asymptotique. Comme application, si on a un circuit calculant le déterminant d'une matrice pour un coût t, alors on peut inverser une matrice (inversible) de la même taille en ct (la constante c étant petite et indépendante de la taille) ; en réduction boîte-noire ce ne sera pas possible pour ce coût là puisque le déterminant ne donne qu'un bit d'information.

> Il y a quelques éléments d'information dans le survey « The Disjunction Property of Intermediate Logics » de Chagrov et Zakharyashchev (*Studia Logica* 1991, <URL: https://www.jstor.org/stable/20015573 >).

Merci, je rajoute ça à mon dossier des n-millions de livres/articles scientifiques que j'ai envie de lire depuis une éternité. (Et j'ai fumé l'autre jour avec mon histoire d'élimination des coupures, quand on rajoute ces schémas d'axiome, bah ça ne marche plus du tout.)

4. Vu que la valeur d'un témoin (d'une promesse) ne compte pas, il est plus intéressant de dire que le programme doit toujours terminer, mais que la valeur retournée n'est consultée que dans l'autre cas.

3. Ah, et est-ce qu'il y aurait un bi-rapport entre typage / réalisabilité et types à la Church / types à la Curry?

1. Plutôt que "promesse", je dirais "témoin".

2. Cette histoire de réalisabilité me rappelle la "computability logic" de Giorgi Japaridze. Mais penser à ce qui est pareil ou diffère me fait mal à la tête.

Encore un commentaire et j'arrête mon monologue, promis. J'ai quand même posé la question sur ≲ à des gens qui s'y connaissent, et on m'a dirigé… vers un obscur papier en Russe de 1968 d'un certain Jankov. <URL:https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/v-a-jankov-constructing-a-sequence-of-strongly-independent-superintuitionistic-propositional-calculi-english-translation-of-xxxvii-2066-by-a-yablonsky-soviet-mathematics-vol-9-no-4-1968-pp-806807-v-a-jankov-the-calculus-of-the-weak-law-of-excluded-middle-english-translation-of-xxxvii-2067-mathematics-of-the-ussrizvestija-providence-vol-2-no-5-for-1968-pub-1969-pp-9971004/A6411145CBFEB629DD444BA00FCA6721> Tiens donc 🙂 Et la réponse est qu'on sait que ≲ n'est pas un beau préordre (à double titre, en fait : ≲ n'est ni bien fondé ni à antichaînes finies).

Ah, c'est ballot. Je reviens au billet, je clique sur le lien « publiée en 2002 », je lis la première phrase de <URL:https://link.springer.com/chapter/10.1007/3-540-45793-3_6> : « It is unknown, whether the logic of propositional formulas that are realizable in the sense of Kleene has a finite or recursive axiomatization. ». Question résolue.

Ouf, Control-P → 24 pages de maths… Heureusement que ça se lit bien. C'est fascinant, merci ! Ça me fait me sentir moins bête que tu aies aussi été surpris que réalisable n'implique pas intuitionnistement prouvable (j'avais conscience de la différence et je pensais vaguement que ça ferait une différence au premier ordre, mais je n'aurais jamais imaginé qu'il y ait déjà une différence au niveau propositionnel). D'une manière générale, j'apprécie vraiment sur ce blog que contrairement à beaucoup de livres de maths, on n'a pas uniquement les faits, mais on le sait quand une affirmation est surprenante, ou bien triviale, ou bien quand une question qu'on a naturellement envie de se poser n'a pas de réponse connue, ou quand une démonstration a l'air simple mais qu'elle a mis 20 ans à être trouvée, …

La question qui me vient immédiatement à l'esprit, c'est : est-ce qu'on sait si l'ensemble des formules réalisables est engendré à partir de la logique intuitionniste en supposant un nombre fini de formules avec leurs raffinements, de même que la logique classique est formée en supposant l'unique formule P ∨ ¬P avec ses raffinements, et que la logique du tiers exclu faible est formée en supposant l'unique formule P ∨ ¬¬P avec ses raffinements ?

Plus précisément, si j'ai une formule F, je peux former un schéma d'axiome

__________________________________ (P1, …, Pn variables, G1, …, Gn formules)
⊢ F[P1:=G1, P2:=G2, …, Pn:=Gn]

Est-ce qu'on obtient les formules réalisables comme ensemble des formules prouvables en rajoutant au calcul des séquents intuitionniste un nombre fini de tels schémas d'axiome ?

Si on savait que oui, ce serait forcément dans ce billet vu que ça clorait complètement la question de « mais qu'est-ce qu'on peut faire exactement pour réaliser une formule ». Est-ce que par hasard, dans le peu qu'on sait de la réalisabilité, on sait quand même que non, ou bien est-ce qu'on ne sait pas ?

Autre point de vue : je peux définir un préordre ≲ sur les formules propositionnelles par X ≲ Y ssi (∀̅ X) ⇒ (∀̅ Y) est prouvable dans la logique propositionnelle intuitionniste du second ordre (où ∀̅ veut dire qu'on quantifie universellement toutes les variables libres, en particulier X ≲ Y est plus faible que « X ⇒ Y intuitionnistement »). La question est alors de savoir si l'ensemble des formules réalisables, qui est clos par le haut et dirigé vers le bas, est un cône, c'est à dire qu'il s'écrit comme ↑{F} := {G | F ≲ G}. Si ≲ est un beau préordre, alors c'est forcément oui, mais je ne crois pas que ≲ soit un beau préordre. Enfin, je ne peux plus réfléchir, là.

D'ailleurs, si c'était oui, alors je crois que le problème de savoir si une formule est réalisable serait automatiquement décidable (on doit pouvoir faire de l'élimination des coupures dans le calcul des séquents enrichi de ces schémas d'axiome pour récupérer la propriété de la sous-formule).