David Madore's WebLog: La réalisabilité propositionnelle, et ce qu'elle nous apprend sur les algorithmes

Introduction : de quoi s'agit-il ? Cadre et motivations

La calculabilité s'intéresse à décrire de façon générale ce que peut ou ne peut pas faire un algorithme informatique. La réalisabilité propositionnelle s'intéresse (du moins selon le point de vue que j'adopte ici) spécifiquement à certaines sortes de manipulations que je pourrais être qualifier de manipulations de données génériques (ou abusivement, fonctions polymorphes). On va décrire ces manipulations génériques par des formules logiques, du style A∧B ⇒ B∧A (logiquement, celle-ci se lit : si A et B alors B et A). La formule représente une sorte de « contrat » qui stipule la manipulation censément effectuée : par exemple, la formule A∧B ⇒ B∧A représente le contrat je prends une donnée de type A et une donnée de type B et je renvoie une donnée de type B et une donnée de type A (et on peut faire ça algorithmiquement, de façon à peu près évidente, en échangeant les deux données qu'on a reçues). Lorsqu'il y a un algorithme qui remplit le contrat, on dira qu'il réalise la formule, ou que celle-ci est réalisable.

Je donnerai une définition précise plus bas de comment lire la formule comme un contrat et ce que ça signifie de la réaliser, mais je peux tout de suite donner un aperçu informel : on s'intéresse à des formules écrites avec les connecteurs binaires ‘∧’, ‘∨’ et ‘⇒’, ainsi que les constantes ‘⊤’ et ‘⊥’ (et ‘¬’ qui est juste une abréviation de X⇒⊥). Les variables (A,B dans l'exemple que je viens de donner) représentent des types de données quelconques et non spécifiés, et les connecteurs logiques représentent des façons de mettre ces données ensemble : grosso modo,

• A∧B (le « et » logique) représente la donnée d'une donnée de type A et d'une de type B,
• A∨B (le « ou » logique) représente la donnée d'une donnée de type A ou d'une de type B (mais avec l'information de laquelle on a),
• A⇒B (l'implication) représente une fonction (au sens informatique) qui prend une donnée de type A et en renvoie une de type B,
• ⊤ (le « vrai ») représente une donnée triviale, et ⊥ (le « faux ») représente une donnée impossible (inexistante ou inobtenable),
• ¬A (la négation) représente une promesse qu'il n'y a pas de A.

Ainsi, par exemple, pour faire une manipulation représentée par la formule (« contrat ») A∧B ⇒ B∧A, on prend une donnée de type A et une donnée de type B et on les renvoie dans l'ordre contraire, c'est-à-dire la donnée de type B et la donnée de type A, et on pourra dire que la formule A∧B ⇒ B∧A est réalisable (et que ce programme la réalise, i.e., il « remplit le contrat »).

J'ai utilisé le terme type ci-dessus, mais il n'est peut-être pas vraiment approprié, parce que justement, la réalisabilité ce n'est pas pareil que le typage, même si ça y ressemble beaucoup (et c'est la différence qui est très intéressante). Je m'explique un peu plus.

Il y a un formalisme appelé correspondance de Curry-Howard (j'en ai parlé dans un billet précédent, dont il est peut être intéressant de lire au moins l'introduction même si ce n'est pas strictement nécessaire pour la suite) qui transforme une démonstration d'une formule dans un certain système logique (le calcul propositionnel intuitionniste) en un programme qui fait la manipulation décrite par cette formule. Et le fait que ce programme fasse bien cette manipulation est attesté par ce qu'on appelle un système de typage, en l'occurrence le λ-calcul simplement typé enrichi de types produits et sommes, 1 et 0 mais peu importe : si on se limite aux programmes conformes à ce système de typage, alors la correspondance est exacte — je veux dire, bijective : on peut vraiment identifier les preuves de tel système logique avec les programmes conformes à tel système de typage. D'ailleurs, la correspondance n'est pas bien compliquée et fait vraiment correspondre de façon assez simple les différentes règles de la logique avec les différentes constructions admises par le système de typage.

Le système de typage (disons ce fameux λ-calcul simplement typé enrichi de types produits et sommes, 1 et 0), il contraint les programmes a priori : il les contraint dans toutes les étapes de leur construction, il exige que toutes les opérations qu'ils font soient conformes au typage. Et au bout du compte, les formules obtenues décrivant les manipulations qu'on peut faire, ce sont justement leurs types (à la notation près), et ce sont exactement les formules démontrables dans le système logique (c'est ça que dit la correspondance de Curry-Howard).

Mais ce n'est pas de ça que je veux parler. Ça c'est ce dont j'ai déjà parlé (dans la première partie du billet sur Curry-Howard).

La réalisabilité[#3], elle ne contraint pas les programmes a priori comme le fait le typage. Elle correspond à la philosophie suivante : le programme a le droit de faire ce qu'il veut comme manips (il faut juste que ce soit un algorithme au sens usuel de la calculabilité, celle de Church-Turing, l'idéalisation standard de ce que c'est qu'un ordinateur) et réaliser une formule ça signifie qu'il remplit un certain contrat. Peut-être qu'entre temps, au sein de leurs manips, les programmes violent toutes les règles du typage, mais au final, on demande juste qu'ils remplissent le contrat représenté par la formule : c'est le résultat qui compte, et seul le résultat qui compte. (Peut-être aussi qu'il est impossible de prouver que le programme remplit bien son contrat, mais ce qui importe c'est que mathématiquement il le fait : là aussi, c'est juste le résultat qui compte.)

[#3] Enfin, la réalisabilité propositionnelle que j'évoque ici, et qu'on peut qualifier de réalisabilité propositionnelle non typée pour insister, parce qu'il y a 1001 variantes de la notion (ce qui a causé un certain dialogue de sourds entre Andrej Bauer et moi dans cette question MathOverflow — sa réponse est très intéressante mais elle ne répond pas vraiment à la question que je voulais poser, quoiqu'elle réponde peut-être à la question que j'ai posée).

Par exemple, A∧B ⇒ B∧A c'est le contrat tu vas recevoir deux données, la première de type A et la seconde de type B (et, précision importante, tu n'auras ni accès ni information sur ce que sont A et B), tu dois terminer en temps fini et renvoyer une donnée de type B et une donnée de type A, et effectivement on peut se convaincre que la seule façon de faire ça c'est d'échanger l'ordre des coordonnées.

Quand la formule est démontrable (en calcul propositionnel intuitionniste) ou, ce qui revient au même par Curry-Howard, quand on peut faire un programme typé correspondant à la formule, alors certainement ce programme remplit le contrat représenté par la formule, donc elle est réalisable.

Mais la grande surprise (en tout cas pour moi quand j'ai appris ça, mais aussi, de ce que je comprends, pour Kleene qui contrairement à moi n'était pas un idiot), c'est que la réciproque n'est pas vraie : il y a des contrats qu'on peut remplir — des formules qu'on peut réaliser — sans que la formule soit prouvable, ou, ce qui revient au même, sans qu'on puisse le faire dans le système de typage naturel dans cette situation (le λ-calcul simplement typé enrichi gnagnagna). Un des buts de ce billet est de donner des exemples de telles formules (jetez un coup d'œil plus bas si vous voulez voir à quoi ça ressemble).

Ces formules réalisables mais non démontrables illustrent donc, si on veut, des choses que peut faire un algorithme, remplissant un contrat de manipulation qui ressemble à du typage, mais qui ne sont pas faisables dans le cadre du typage — en tout cas du typage le plus naturel dans cette situation — ou, si on veut, ces choses sont faisables, mais la vérification que le contrat est bien rempli est plus compliquée qu'une vérification locale telle que fournie par le typage.

Bien sûr, il n'y avait aucun doute que les algorithmes généraux sont plus généraux que les algorithmes typés : notamment, les systèmes de typage que j'évoque dans cette introduction ne permettent pas de faire de boucle infinie, donc il est évident qu'ils limitent structuralement les algorithmes. Mais ce qui est surprenant dans l'histoire, c'est que l'algorithme va quand même remplir un contrat qui se lit exactement comme un type, i.e., ils font des manipulations de données génériques potentiellement utiles, pas quelque chose comme une boucle infinie ni même une fonction sur un type spécifique comme les entiers.

Je précise pour dissiper un possible malentendu que ce que je dis là n'est pas destiné à être une attaque contre le typage ou son utilité, juste un signe que les choses sont plus délicates que ce qu'on pourrait imaginer naïvement : certes Curry-Howard nous dit que les formules logiques qui correspondent à des programmes typés sont exactement les formules démontrables, mais il y a des contrats qu'on peut remplir de façon plus subtile que le typage.

Et du coup, il me semble que c'est un problème très naturel pour l'informatique et la calculabilité que d'étudier cette réalisabilité propositionnelle, parce que ça a directement trait à ce qu'un algorithme peut ou ne peut pas faire. (Notons que c'est là l'approche que je donne à la question dans ce billet, tout le monde ne sera pas forcément d'accord que c'est la bonne motivation.)

Organisation de ce billet

Dans la suite, je commence par définir de façon précise ce que c'est que la réalisabilité propositionnelle, et je donne des exemples très simples d'une formule réalisable (A∧B ⇒ B∧A) et d'une formule qui ne l'est pas (A ∨ ¬A) pour montrer comment on manie la notion. Ensuite je dois faire un certain nombre de remarques générales (plusieurs desquelles sont en petits caractères pour montrer qu'on peut les ignorer et passer à la suite).

Puis je me tourne vers des exemples de formules réalisables mais non démontrables, parce que c'est quand même ça la grosse surprise, que de telles formules existent : pour chacune, j'ai essayé de donner non seulement un algorithme qui la réalise (et comment il fonctionne) mais aussi des explications informelles à son sujet. En revanche, je ne détaille pas l'argument expliquant que la formule n'est pas démontrable (en calcul propositionnel intuitionniste) : il n'y a que la première pour laquelle j'ai fait cet effort, et encore succinctement et en petits caractères, parce que ce n'est pas vraiment mon sujet.

Je commence par la formule qui me semble la plus simple à comprendre intuitivement, celle de Ceitin, puis j'en passe en revue un certain nombre d'autres. On peut traiter ça comme autant d'énigmes : une fois qu'on a compris le principe, c'est un petit jeu de regarder chaque formule comme un contrat à remplir et de se demander comment je vais faire une telle chose avec un algorithme ? (en tout cas, c'est comme ça que j'ai approché le problème : je n'ai pas lu les preuves de réalisabilité qu'on trouve dans la littérature, c'était bien plus instructif de les retrouver moi-même).

Ensuite, je passe à des exemples de formules non réalisables mais intéressantes et notamment « presque » réalisables, à travers deux exemples importants : la formule de Kreisel-Putnam et celle de Scott. Donc cette fois il faut à la fois montrer qu'elles ne sont pas réalisables et que, pourtant, on ne passe pas loin de l'être (et j'explique en quoi elles sont « presque » réalisables, même si je n'ai pas réussi à avoir le recul pour comprendre si on peut définir cette notion proprement).

Enfin je finis par des généralités et spéculations peut-être vaseuses et certainement mal écrites, qui font un peu le pendant de l'introduction ci-dessus.

Pourquoi j'estime que c'est intéressant et important

Bien sûr, comme je l'explique ci-dessus, on peut traiter chacune des formules que je vais lister ci-dessous (aussi bien celles qui sont réalisables que celles qui ne le sont pas) comme un exercice de calculabilité : voici une formule représentant un certain contrat, trouver une façon de le remplir [= réaliser la formule] ou montrer que ce n'est pas possible ; ou même comme une sorte d'énigme (à la manière dont je l'ai fait ici et là). Les outils de base utilisés par ces algorithmes sont toujours un peu les mêmes, et ce sont les techniques fondamentales de la calculabilité : lancer deux tâches en parallèle (sachant qu'au moins une des deux terminera), exécuter un programme pour un certain nombre d'étapes pour voir s'il termine, parcourir tous les entiers naturels en sachant qu'on finira par en trouver un qui remplit une certaine condition — ce genre de choses qui sont les bases de la calculabilité de Church-Turing. Donc déjà c'est au moins intéressant parce que c'est instructif à ce niveau-là.

Mais je pense que ça va plus loin que ça. Comme je le dis plus haut, la réalisabilité propositionnelle est une façon d'aborder le problème, qui me semble central en informatique, de ce qu'un algorithme peut ou ne peut pas faire, et en l'occurrence il est important de comprendre ce que le typage laisse ou ne laisse pas passer, et comme le typage est un outil lui aussi central, comprendre ce qu'il ne laisse pas passer est justement une question cruciale, et même si on peut trouver que la réalisabilité propositionnelle est un prisme un peu étroit pour étudier cette question (j'en conviens), je pense qu'elle a des choses à dire, et je n'ai pas l'impression qu'on les comprenne bien dans l'état actuel de l'art (d'où le fait que les exemples de formules réalisables soient un peu… hétéroclites), mais ça vaut certainement la peine de méditer un peu sur chacune de ces formules certes disparates et de ce qu'elle signifie et ce qu'elle représente. En tout cas, ce n'est certainement pas un hasard si la réalisabilité de ces différentes formules fait appel à ce que je viens d'appeler les techniques fondamentales de la calculabilité.

En outre, ça nous apprend aussi — il me semble — des choses sur la richesse de la logique intuitionniste, même au niveau simplement propositionnel (en nous forçant à nous demander ce que disent logiquement certaines de ces formules qu'on n'aurait sans doute pas pensé à considérer sinon). Ma motivation à moi était justement de me familiariser mieux à la fois avec la calculabilité en général et avec les techniques à l'interface entre logique, calculabilité et typage : en réexpliquant chacune de ces preuves, je m'assure que je les ai bien comprises. (Et il y a plein de choses que j'ai été obligé de revoir en écrivant ce billet.)

Pour une perspective plus approfondie, bien sûr, il faut se tourner vers le topos effectif : j'ai déjà écrit un billet à son sujet, et même si je précise que je n'y ferai pas référence dans la suite (sauf en passant, mais en tout cas il n'est pas nécessaire d'avoir lu ledit billet ; au contraire, l'ordre logique serait sans doute plutôt de commencer par celui-ci), le topos effectif est en filigrane dans toute cette histoire, parce que la réalisabilité propositionnelle est la logique (propositionnelle) interne du topos effectif. Si on croit que le topos effectif est une formalisation raisonnable du monde des mathématiques effectives, alors la réalisabilité propositionnelle est un sujet certainement important parce qu'elle correspond aux modes de raisonnement purement logiques qui sont admissibles dans ce monde des mathématiques effectives. (Et, encore une fois, c'est une surprise que ces modes de raisonnement dépassent la pure logique intuitionniste, parce qu'il y a des formules réalisables mais non intuitionnistement démontrables : on a affaire à une logique intermédiaire strictement située entre la logique intuitionniste et la logique classique, et elle est très mal comprise.)

J'en profite pour mentionner deux choses que je n'ai pas eu le courage d'évoquer (ou à peine et en petits caractères) : il y a deux extensions au cadre purement propositionnel que je ne fais qu'effleurer ici mais qui me semblent très intéressants. La première est l'addition de quantificateurs portant sur les variables propositionnelles : côté logique ou typage cela revient à passer à ce qui s'appelle la logique propositionnelle du second ordre et le système F de Girard, et il y aurait assurément des formules réalisables non démontrables intéressantes à trouver dans ce cadre comme il y en a dans le cadre propositionnel simple qui est l'objet central de ce billet. La seconde extension consiste à ajouter des modalités à la logique : or il se trouve que la notion d'oracle est précisément et parfaitement décrite par ce qui s'appelle des topologies de Lawvere-Tierney sur le topos effectif et qui donnent lieu, au niveau logique, à des modalités ; j'avais essayé d'expliquer le premier point (sans parler du topos effectif !) dans ce très long billet, donc normalement j'aurais dû essayer de tisser un lien entre les deux, mais j'avoue que le courage m'a manqué, donc en fait ils sont complètement indépendants.

Prérequis et rapport à d'autres billets

Ce billet présuppose connues les bases de la théorie de la calculabilité : essentiellement, la notion de fonction générale récursive ou machine de Turing et leurs propriétés de base. Le contenu du premier jeu de transparents de mon cours à Télécom contient largement plus que ce qui est nécessaire (on peut notamment ignorer tout ce qui parle de fonctions primitives récursives). Mais en fait, ce n'est pas tellement une question de connaissances préalables nécessaire, que d'habitude du raisonnement mathématique/informatique consistant à écrire un algorithme qui va lui-même prendre en argument un algorithme qui va lui-même essayer d'exécuter un algorithme, etc. : je suppose mon lecteur familier avec ce genre de choses.

En revanche, je ne présuppose la lecture d'aucun billet précédent dans ce blog. Même si la lecture de la première partie de celui sur Curry-Howard intitulée le cas du calcul propositionnel sera utile, j'ai déjà dit dans l'introduction l'essentiel de ce qu'il faut savoir sur Curry-Howard. La notion de démonstration en calcul propositionnel intuitionniste n'est pas non plus vraiment aussi importante qu'on pourrait le croire dans ce billet-ci, donc je me contente d'en rappeler brièvement les règles plus bas (elles sont déjà dans le billet que je viens de lier sur Curry-Howard, ou si on préfère de ce billet ou celui-ci).

Même si je ne suppose pas qu'on a lu autre chose sur ce blog, je peux néanmoins dire quelque chose sur la position logique de ce billet par rapport à d'autres entrées précédentes. Si on a lu celle sur le topos effectif, cette entrée-ci est beaucoup plus simple techniquement parce qu'il s'agit ici juste de la partie purement propositionnelle de la logique interne du topos effectif, que je vais commencer par redéfinir de novo. De même, j'avais déjà écrit des choses ici sur la réalisabilité en logique du premier ordre, donc là aussi, c'est un peu la même chose mais en plus simple (quoique pas tout à fait un sous-ensemble non plus : j'explique plus bas le rapport, qui est malheureusement un peu confus). Comme je l'ai écrit plus haut, je n'ai pas eu le temps/courage de faire le lien avec ce très long billet sur les oracles en calculabilité, donc il n'y aura que quelques allusions.

Par ailleurs, je vais dévoiler plus bas que cette énigme et celle-ci étaient en fait une façon cachée d'exprimer respectivement la réalisabilité et l'irréalisabilité de certaines formules propositionnelles.

*

Une source importante pour ce billet est le survey (en anglais) de Valery Plisko, A Survey of Propositional Realizability Logic (Bull. Symbolic Logic 15 (2009) 1–42) : si je parle du survey de Plisko c'est à ce texte que je fais référence.

Les opérations ‘⊓’, ‘⊔’ et ‘⇛’

De quoi s'agit-il, donc ? Le cœur de la réalisabilité propositionnelle est de définir trois opérations binaires ‘⊓’, ‘⊔’ et ‘⇛’ entre ensembles, qui correspondent grosso modo à une sorte de produit cartésien, de réunion disjointe et d'ensemble de fonctions, mais dans une forme calculable/informatique. Je vais donner leur définition en une version plutôt matheuse et une version plutôt informaticienne, mais il va de soi qu'elles sont fonctionnellement équivalentes. Je donne les deux pas juste dans l'espoir d'intéresser plus de public (même s'il y a de ça), mais aussi parce que les deux ont quelque chose à nous apprendre.

(Je précise que c'est moi qui note ces opérations ‘⊓’, ‘⊔’ et ‘⇛’. Il est plus standard de les noter ‘∧’, ‘∨’ et ‘⇒’ — voire ‘→’ — parce qu'ils vont servir d'interprétation des connecteurs propositionnels en question ; mais je trouve pédagogiquement plus clair de commencer par les noter différemment. Dans les transparents de mon cours à Télécom — deuxième partie — je les ai notés avec un petit point au-dessus, c'est-à-dire quelque chose comme ‘∧̇’, ‘∨̇’ et ‘⇒̇’, ce qui est plus léger que d'avoir des jeux complètement distincts de symboles, mais en HTML cette notation avec un point est problématique à divers titres, donc ici je préfère les symboles bien distincts ‘⊓’, ‘⊔’ et ‘⇛’. Plus bas dans ce billet, quand j'estimerai avoir suffisamment éclairci les choses pour qu'il n'en résulte pas de confusion, je me permettrai peut-être de traiter ‘⊓’, ‘⊔’ et ‘⇛’ comme vaguement interchangeable avec ‘∧’, ‘∨’ et ‘⇒’ sauf quand je veux souligner la distinction, mais pour l'instant je fais l'effort de séparer les deux jeux de symboles.)

Commençons par la version matheuse : je définis trois opérations ‘⊓’, ‘⊔’ et ‘⇛’ sur l'ensemble 𝒫(ℕ) des parties de ℕ (i.e., formellement, trois fonctions 𝒫(ℕ)² → 𝒫(ℕ)), de la manière suivante : pour P et Q deux ensembles d'entiers naturels :

• P⊓Q l'ensemble des ⟨p,q⟩ pour p∈P et q∈Q où ⟨p,q⟩ est un codage des couples d'entiers naturels par des entiers naturels (par exemple on peut décréter que ⟨p,q⟩ := p + ½(p+q)(p+q+1), même si la formule n'a évidemment pas d'importance, la seule chose qui compte est que ce soit une bijection calculable de ℕ² sur ℕ, et d'ailleurs « injection » suffit). Autrement dit, ce sont les codes des couples dont la première composante est dans P et la seconde dans Q (c'est donc juste l'image du produit cartésien P×Q par la fonction codage des couples ⟨—,—⟩).

• P⊔Q l'ensemble des ⟨0,p⟩ pour p∈P et des ⟨1,q⟩ pour q∈Q, i.e., la réunion disjointe d'une copie {0}⊓P de P et d'une copie {1}⊓Q de Q. Autrement dit, c'est un codage de la réunion disjointe de même que le point précédent était un codage du produit cartésien. La première composante du couple (0 ou 1) sert donc à indiquer dans quelle composante on se trouve.

• P⇛Q l'ensemble des e∈ℕ tels que la fonction générale récursive codée par l'entier e soit totalement définie sur P et l'envoie à l'intérieur de Q. Autrement dit, si j'appelle e•p (ce qui est souvent noté φ_e(n) — ou parfois {e}(n) dans des textes un peu poussiéreux) désigne la valeur en p de la e-ième fonction générale récursive (= partielle calculable) dans une énumération standard, alors il s'agit des e tels que pour tout p∈P on ait e•p↓∈Q (ceci signifiant que d'une part e•p est défini et d'autre part que l'entier en question appartient à Q).

Dans la version plus informaticienne de la définition, je vais plutôt parler d'ensembles de « données binaires », et supposer que j'ai affaire à un ordinateur abstrait (équivalent à une machine de Turing) capable de manipuler de telles données binaires :

• P⊓Q l'ensemble des données binaires représentant (d'une certaine manière fixée à l'avance) un couple ⟨p,q⟩ de données binaires p∈P et q∈Q.

• P⊔Q l'ensemble des données binaires représentant (d'une certaine manière fixée à l'avance) une union avec sélecteur contenant soit un p∈P soit un q∈Q (le sélecteur servant à retenir si on est dans le premier cas ou dans le second).

• P⇛Q l'ensemble des données binaires e qui représentent un programme (pour la machine considérée) qui, quand on l'exécute sur une entrée p∈P, va terminer et produire un résultat dans Q.

On peut objecter que ces deux définitions sont exactement la même chose (oui, c'est le but…), et que la seconde est juste moins précise, mais je trouve qu'elle est quand même pertinente et pas juste dans le sens d'être plus facile à lire, parce que certaines des remarques qui suivent ont vraiment plus de sens dans cette optique. En tout cas, je me permettrai de passer librement de l'une à l'autre, et par exemple de dire que e∈ℕ est un programme qui prend un élément de P et renvoie un élément de Q pour exprimer la condition d'appartenir à P⇛Q.

Remarques sur ces trois opérations, donc :

• Si on est familier avec les concepts de typage, les opérations ‘⊓’, ‘⊔’ et ‘⇛’ ont évidemment un rapport avec les opérations ‘×’, ‘+’ et ‘→’ (représentant les types produit, somme et fonction) respectivement dans un système de typage, et cette question va revenir ci-dessous, mais en attendant je souligne que je ne parle pas de typage ici dans ma définition.

  Notamment, mon langage de programmation évoqué dans la définition « informatique » n'est pas typé (et c'est pour ça que je parle de « données binaires ») ; ou s'il est typé, c'est de façon superficielle/dynamique, comme Python, Perl et compagnie (c'est-à-dire qu'on a évidemment le droit de se décréter, si l'on veut, que le langage ne mélange pas la représentation des couples et des programmes ! et donc que si on cherche à exécuter comme programme quelque chose qui n'en est pas un, que ça produit une erreur : pour la théorie que j'expose ici, « une erreur » sera traité de façon identique à une boucle infinie, c'est le plus simple ; mais cette erreur ne se produit qu'à l'exécution).

• Les opérations ‘⊓’, ‘⊔’ et ‘⇛’ sont évidemment inspirées, si on sait ce que c'est, par l'interprétation informelle de Brouwer-Heyting-Kolmogorov de la logique propositionnelle intuitionniste (cf. ce bout de ce billet passé si on veut en savoir plus). Il s'agit effectivement d'une tentative de rendre rigoureuse cette interprétation intuitive. (Et c'est notamment pour cette raison que c'est une surprise que la sémantique ne va pas coïncider avec la « pure » logique intutionniste.)

• Une des conséquences du théorème de Rice est qu'il est impossible de décider de façon générale l'appartenance à P⇛Q dans n'importe quel cas non-trivial (i.e., sauf si c'est vide ou plein). Ce n'est pas une erreur.

  C'est déjà là une différence profonde avec le typage : en typage, on sait par construction quelle donnée a quel type. En réalisabilité, en gros dès qu'il y a une flèche dans l'histoire, c'est indécidable.

• On notera comme cas particulier de la définition que P⇛∅ est vide si P est habité (= non vide), car la condition que la valeur de retour appartienne à ∅ est impossible à satisfaire ; en revanche P⇛∅ est plein lorsque P est vide (car il n'y a aucune condition imposée).

  Je noterai ☇P comme abréviation de P⇛∅ (notation vraiment pas standard du tout, mais qui s'avérera utile : j'avais commencé à écrire ce billet sans, mais avoir un équivalent au niveau de ‘⊓’, ‘⊔’ et ‘⇛’ de ce qu'est ‘¬’ pour ‘∧’, ‘∨’ et ‘⇒’ est quand même utile).

  On dira que les éléments de ☇P := (P⇛∅) sont des promesses que P est vide. (Le mot promesse n'a pas ici le sens qu'il a, disons, en JavaScript : une promesse que P est vide est, ici, simplement n'importe quelle donnée si P est vide, et ça n'existe pas si P n'est pas vide.) A contrario, les éléments de ☇☇P := (P⇛∅)⇛∅ sont des promesses que P est habité (= non vide). Le terme de promesse sert simplement à souligner qu'il s'agit d'une donnée sans aucun contenu informatif à part la véracité de la chose qu'elle promet (les promesses sont toujours interchangeable : si n est une promesse valable de quelque chose, alors 42 en est une).

• Un élément de P⇛Q qui reçoit un élément qui n'est pas dans P en entrée a le droit de faire n'importe quoi avec : ne pas terminer, renvoyer un élément qui n'est pas dans Q, ou n'importe quoi d'autre. (Mais « n'importe quoi » c'est quand même « n'importe quoi » dans le cadre de la calculabilité de Church-Turing : il n'a pas le droit de vous tuer — je précise ça, parce qu'on aura besoin plus bas de la technique consistant à lancer plusieurs calculs en parallèle, dont seulement certains donneront un résultat correct : ce ne serait pas envisageable si les calculs lancés sur une donnée « incorrecte » avaient le droit de causer des dommages ou quelque chose du genre. C'est pour ça que je n'utilise pas le terme, consacré dans un certain milieu informaticien, de démons nasaux.)

Formules réalisables

Considérons maintenant les formules propositionnelles, c'est-à-dire les formules logiques (du genre A∧B⇒B∧A ou bien (A⇒B)∨(B⇒A)) fabriquées à partir d'un stock illimité de variables propositionnelles (ici notées A,B,C,…) au moyen des opérations binaires (connecteurs logiques) :

• ‘∧’, représentant la conjonction (et logique),
• ‘∨’, représentant la disjonction (ou logique),
• ‘⇒’, représentant l'implication,

— ainsi que des opérations nullaires (= constantes logiques) ‘⊤’ représentant le vrai et ‘⊥’ représentant le faux. On conviendra que ¬X est une abréviation de notation pour X⇒⊥ (si X alors absurdité), et que X⇔Y est une abréviation de notation pour (X⇒Y)∧(Y⇒X).

Convention habituelles d'écriture : sur la priorité des opérations : ‘¬’ est prioritaire sur ‘∧’, qui est prioritaire sur ‘∨’, qui est prioritaire sur ‘⇒’ et ‘⇔’, et on ne précise rien sur la priorité relative de ‘⇒’ et ‘⇔’ (c'est-à-dire qu'on s'interdira de les mélanger) ; et sur l'associativité, on précise que ‘∧’ et ‘∨’ s'associent à gauche, ce qui n'aura aucune importance, et que ‘⇒’ s'associe à droite (c'est-à-dire que X⇒Y⇒Z doit se comprendre comme X⇒(Y⇒Z)), et on ne précise rien sur ‘⇔’ (c'est-à-dire qu'on s'interdira d'en mettre plusieurs au même niveau sans parenthèses).

Si φ(A,B,C,…) est une telle formule propositionnelle et P,Q,R des parties de ℕ, on peut définir une partie ⟦φ⟧(P,Q,R,…) de ℕ en remplaçant chaque variable propositionnelle A,B,C,… par l'ensemble P,Q,R,… qu'on a choisi de lui associer, et chaque connecteur ‘∧’, ‘∨’, ‘⇒’, ‘⊤’ et ‘⊥’ par ‘⊓’, ‘⊔’, ‘⇛’, ‘ℕ’ et ‘∅’ respectivement. (Je prends le point de vue avec des parties de ℕ plutôt que des ensembles de « données binaires », mais on aura compris que ça ne change rien.) C'est-à-dire précisément :

• ⟦A⟧ = P la partie qu'on a choisie comme affectée à la variable A (ma notation n'est pas très correcte, du coup, mais j'espère qu'on comprend)
• ⟦φ∧ψ⟧ = ⟦φ⟧⊓⟦ψ⟧
• ⟦φ∨ψ⟧ = ⟦φ⟧⊔⟦ψ⟧
• ⟦φ⇒ψ⟧ = ⟦φ⟧⇛⟦ψ⟧
• ⟦⊤⟧ = ℕ disons[#4]
• ⟦⊥⟧ = ∅
• (et notamment ⟦¬φ⟧ = ⟦φ⟧⇛∅, que j'ai noté ☇⟦φ⟧)

[#4] Je précise que même s'il est plus simple ici de prendre ℕ (comme ensemble de réalisateurs de ⊤), ça ne changerait rien d'important si je prenais, disons, {0} (ou, en fait, n'importe quel ensemble habité fixé) à cet endroit dans cette définition. La raison pour laquelle je le précise est pour souligner que ce qui importe ici n'est pas que l'ensemble soit plein (à la différence de la sémantique des ouverts qui sera brièvement évoquée plus bas, où le vrai s'interprète vraiment par l'ensemble plein) mais qu'il soit trivial d'en produire un élément.

Note : Je ferai la même convention sur la priorité des opérations ‘☇’, ‘⊓’, ‘⊔’ et ‘⇛’ (à savoir : décroissante dans cet ordre) que pour ‘¬’, ‘∧’, ‘∨’, et ‘⇒’ qui leur correspondent respectivement. De même pour l'associativité : P⇛Q⇛R doit se lire comme P⇛(Q⇛R) — mais je ne crois pas que ce cas de figure se produise dans ce qui suit.

On dit qu'une telle formule logique φ(A,B,C,…) est réalisable (ou, plus précisément, uniformément réalisable) lorsqu'il existe un même élément qui appartient à ⟦φ⟧(P,Q,R,…) quelles que soient les parties P,Q,R,… par lesquelles on ait remplacé les variables propositionnelles A,B,C,… de la formule. Autrement dit, l'intersection

⋂_{P,Q,R,… ⊆ ℕ} ⟦φ⟧(P,Q,R,…)

est habitée (= non vide). Un tel élément est appelé un réalisateur (ou, plus précisément, un réalisateur uniforme de la formule ; tandis qu'un élément de ⟦φ⟧(P,Q,R,…) peut (abusivement) être qualifié de réalisateur de la formule pour ce choix P,Q,R,… de parties).

(On peut préférer noter quelque chose comme r ⊪ φ — la notation n'est pas très standard — pour dire que r réalise φ, et se dispenser d'expliciter les opérations ‘⊓’, ‘⊔’ et ‘⇛’ au profit de règles du style on a e ⊪ (φ⇒ψ) lorsque, pour tout p tel que p ⊪ φ, on a e•p↓ et e•p ⊪ ψ : c'est ce que j'avais fait dans ce billet. Mais si on préfère ce point de vue-là, il faut que je souligne que quand j'écris r ⊪ φ(A,B,C,…) avec des variables propositionnelles A,B,C,… laissées libres, je veux parler de réalisabilité uniforme pour toutes les parties, i.e., r ⊪ φ(P,Q,R,…) pour un même r quelles que soient P,Q,R,…)

Je souligne que le réalisateur non seulement doit être le même pour toutes les parties P,Q,R,… pour lesquelles il doit réaliser la formule, mais qu'il n'a absolument pas accès à l'information de ce que sont ces parties. Ce sera plus clair sur des exemples.

Avertissement sur un abus de langage : comme je l'ai défini ci-dessus, la phrase r réalise φ(A,B,C,…) signifie que r appartient à ⋂_{P,Q,R,… ⊆ ℕ} ⟦φ⟧(P,Q,R,…) (intersection sur toutes les parties). Néanmoins, une fois choisies des parties P,Q,R,…, il est parfois tentant d'utiliser aussi la phrase r réalise φ(P,Q,R,…) pour dire que r appartient à ⟦φ⟧(P,Q,R,…) (pour ces parties-là) : le fait que les parties soient nommées différemment des variables propositionnelles devrait permettre d'éviter la confusion, donc ce n'est pas bien grave. Sauf que, en fait, au bout d'un moment, je vais me mettre à utiliser les mêmes lettres. J'ai essayé de traquer tous les endroits où j'avais pu commettre cet abus et écrire à chaque fois r appartient à P⇛Q plutôt que r réalise P⇒Q, mais il est plausible que certains m'aient échappé. (Le cas typique est le suivant : si je parle d'un programme qui réalise φ⇒ψ, il est tentant de dire qu'il prend en entrée un entier qui réalise φ et en renvoie un qui réalise ψ, or ce que qu'on veut vraiment dire est que pour tout p qui appartient à ⟦φ⟧(P…) pour certains P,…, appliquer r à p renvoie un élément de ⟦ψ⟧(P…) pour ce même P,…)

Deux exemples simples

Je vais donner deux exemples très simples (une formule réalisable et une formule qui ne l'est pas) qui devraient, j'espère, illustrer la manière dont fonctionne la définition ci-dessus, même si, à ce stade, on ne va pas du tout voir la différence avec le typage.

Considérons d'abord le cas de la formule déjà évoquée dans l'introduction :

A∧B ⇒ B∧A

J'affirme que celle-ci est réalisable. Autrement dit, il s'agit de montrer qu'il existe un même élément qui appartienne à

P⊓Q ⇛ Q⊓P

quels que soient P,Q ⊆ ℕ. Un tel élément est donc un programme qui va prendre en entrée un élément de P⊓Q, c'est-à-dire le codage ⟨p,q⟩ d'un couple formé de p∈P et q∈Q, et il est censé terminer et renvoyer un élément de Q⊓P, autrement dit le codage ⟨q′,p′⟩ d'un couple formé de q′∈Q et p′∈P. On notera que le programme n'a pas accès à la donnée de P et Q (on ne voit pas comment cette donnée pourrait lui être présentée, du reste : ce sont des ensembles possiblement infinis, non-calculables, etc.) : c'est le sens du mot uniformément dans l'histoire. Néanmoins, en l'occurrence, c'est très facile de faire ce qui était demandé : il suffit de prendre le couple ⟨p,q⟩, de le décoder, d'échanger l'ordre des composantes, et de renvoyer le couple ⟨q,p⟩ avec les mêmes éléments dans l'autre ordre. Ce programme appartient manifestement à tous les P⊓Q ⇛ Q⊓P. Autrement dit, il réalise (uniformément !) la formule A∧B ⇒ B∧A. Je dis donc que la formule A∧B ⇒ B∧A est (uniformément) réalisable.

*

Montrons à l'inverse que la formule

A ∨ ¬A

(qui je rappelle est une abréviation de notation pour A ∨ (A⇒⊥)) n'est pas réalisable. Il s'agit donc de montrer qu'il n'y a pas d'élément r qui appartienne à P ⊔ (P⇛∅) pour tout P⊆ℕ : ici, je rappelle que P⇛∅, aussi noté ☇P, est vide lorsque P est habité, et plein lorsque P est vide. Supposons par l'absurde qu'un tel r existe. En considérant le cas P=∅ on voit que r doit être de la forme ⟨1,q⟩ (i.e., il doit sélectionner la seconde composante de la réunion disjointe), tandis qu'en considérant le cas P=ℕ on voit que r doit être de la forme ⟨0,p⟩ (i.e., il doit sélectionner la première composante de la réunion disjointe). Ceci est contradictoire : un tel r (uniforme !) n'existe pas.

Je souligne que c'est l'uniformité qui est vraiment critique ici : quelle que soit la partie P⊆ℕ, l'ensemble P ⊔ (P⇛∅) a un élément : si P est vide, tout ⟨1,q⟩ est dedans, tandis que si P est habité, tout ⟨0,p⟩ avec p∈P est dedans. Mais il n'y a pas de réalisateur commun (= « uniforme ») pour toutes les parties P⊆ℕ.

La rédaction informelle de l'argument ci-dessus est quelque chose comme ceci : Un réalisateur (uniforme) de A ∨ ¬A est censé être soit un élément d'une partie P soit une promesse du fait qu'elle est vide, et ce, sans avoir accès à la partie P : ce n'est manifestement pas possible car il ne peut pas deviner si elle est habitée ou non.

Remarque sur l'uniformité et la version non-uniforme

Je l'ai déjà dit plusieurs fois, mais faisons-en une belle tartine : ce qui m'intéresse, c'est la réalisabilité uniforme, c'est-à-dire la question de l'existence d'un même r qui appartienne à ⟦φ⟧(P,Q,R,…) quelles que soient les parties P,Q,R,…

Que se passerait-il si on demandait simplement que ⟦φ⟧(P,Q,R,…) soit habité quelles que soient les parties P,Q,R,… mais pas forcément par le même élément ? Appelons ça non-uniformément réalisable (même si je vais justement expliquer que ce n'est pas une notion très intéressante). Il est facile de remarquer que :

• P⊓Q est habité si et seulement si P et Q le sont,
• P⊔Q est habité si et seulement si P ou Q l'est,
• P⇛Q est habité si et seulement si ‹si P est habité alors Q l'est› (i.e., lorsque soit Q est habité soit P est vide ; en effet, pour le premier cas, il suffit de considérer le programme renvoyant constamment un élément q donné de Q, et pour le second il n'y a rien à faire donc P⇛Q vaut ℕ).

(Je travaille — de façon externe — en logique classique, donc le mot habité est juste une façon de dire non vide tout en évitant de multiplier les négations confuses.)

De là il résulte que ⟦φ⟧(P,Q,R,…) est habité, pour des parties P,Q,R,…, si et seulement si la formule obtenue en remplaçant les variables A,B,C,… de φ par vrai ou faux selon que la partie (P,Q,R,…) choisie est habité ou non, a la valeur de vérité vrai. Bref, ceci prouve :

Proposition : La formule φ(A,B,C,…) est non-uniformément réalisable (i.e., ⟦φ⟧(P,Q,R,…) est habité non-uniformément quelles que soient les parties P,Q,R,…) si et seulement si la formule φ(A,B,C,…) est classiquement vraie (c'est-à-dire que toutes les cases de son tableau de vérité obtenu en considérant toutes les façons de remplacer chacune des variables par vrai ou faux).

Le si généralise ce que j'ai observé sur l'exemple de A ∨ ¬A donné plus haut (cette formule, classiquement vraie, n'est certes pas uniformément réalisable, mais chaque instance où on a remplacé A par une partie P de ℕ est réalisable). Mais le seulement si est intéressant aussi : il implique que toute formule non-uniformément réalisable, et notamment toute formule (uniformément) réalisable, est classiquement vraie. Ainsi, on n'a aucun espoir de réaliser uniformément la formule (A∨B)⇒(A∧B), par exemple, parce qu'elle n'est même pas vraie pour toutes valeurs de vérité booléennes mises à la place de A,B.

Correction de la sémantique : les formules démontrables sont réalisables

On dit que la formule φ est démontrable selon les règles de la logique propositionnelle intuitionniste (ou intuitionnistement démontrable, ou constructivement valable, ou simplement démontrable si c'est clair dans le contexte qu'on parle de logique intuitionniste), si elle s'obtient sans hypothèse à partir des règles suivantes :

(Hypothèse)

Si un énoncé fait partie des hypothèses courantes, alors on peut l'affirmer (i.e., elle est démontrée sous ces hypothèses).

(Introduction du ‘⇒’)

Si sous une hypothèse φ (c'est-à-dire : en rajoutant celle-ci aux hypothèses en cours) on a démontré ψ, alors, sans cette hypothèse (c'est-à-dire en la déchargeant), on peut en tirer φ⇒ψ.

(Élimination du ‘⇒’ ou modus ponens)

Si on a démontré φ⇒ψ et qu'on a démontré φ, alors on peut en tirer ψ.

(Introduction du ‘∧’)

Si on a démontré ψ₁ et ψ₂, alors on peut en tirer ψ₁∧ψ₂.

(Élimination du ‘∧’)

Si on a démontré ψ₁∧ψ₂, alors on peut en tirer ψ₁, et on peut en tirer ψ₂.

(Introduction du ‘∨’)

Si on a démontré ψ₁, ou si on a démontré ψ₂, alors on peut en tirer ψ₁∨ψ₂.

(Élimination du ‘∨’ ou raisonnement par cas)

Si on a démontré φ₁∨φ₂, et si sous l'hypothèse φ₁ on a démontré ψ et que sous l'hypothèse φ₂ on a aussi démontré la même conclusion ψ, alors on peut tirer ψ de tout ça (sans aucune des hypothèses φ₁ et φ₂, c'est-à-dire en les déchargeant).

(Introduction du ‘⊤’)

On peut démontrer ⊤.

(Élimination du ‘⊥’ ou ex falso quodlibet)

Si on a démontré ⊥, on peut en tirer ψ absolument quelconque.

(Je cite les règles ici juste pour mémoire, et je ne vais pas m'appesantir dessus parce que je ne vais pas avoir besoin d'entrer dans leur détail. Je les expliquées plus en détail dans plusieurs billets passés, notamment celui-ci, et avec des présentations différentes dans celui-ci ou celui-là.)

À titre d'exemple, la formule A∧B⇒B∧A est intuitionnistement démontrable (par la règle d'introduction du ‘⇒’, il suffit de montrer B∧A sous l'hypothèse A∧B ; or sous cette hypothèse, on a A et B par les règles d'élimination du ‘∧’, donc B∧A par la règle d'introduction du ‘∧’, comme on voulait).

Le rapport entre démontrabilité et réalisabilité est fourni par le résultat suivant :

Théorème (correction de la sémantique de la réalisabilité propositionnelle) : Si formule φ(A,B,C,…) est intuitionnistement démontrable, alors elle est (uniformément !) réalisable.

(Je ne sais pas bien à qui attribuer ce théorème, qui n'est pas bien difficile : peut-être un sous-ensemble de Dragalin, Troelstra et Nelson. Ces gens ont certainement prouvé des choses de ce genre, mais la notion de réalisabilité avec laquelle ils travaillaient n'était pas exactement la mienne ici.)

La preuve de ce théorème est essentiellement fournie par la correspondance de Curry-Howard, et elle est constructive : c'est-à-dire qu'on convertit la démonstration intuitionniste de φ en un programme (en transformant chaque règle de la logique en une construction au niveau des programmes), et ce programme fournit un réalisateur de la formule. Les détails sont dans ce billet (plus exactement dans la partie de celui-ci qui concerne le cas propositionnel), je n'insiste pas plus ici.

Comme je le dis ci-dessus, la formule A∧B⇒B∧A est intuitionnistement démontrable ; et si on convertit la démonstration que j'ai donnée en programme par la correspondance de Curry-Howard, on obtient précisément le programme (noté λ(z:A∧B). ⟨π₁z, π₂z⟩ dans la notation de mon billet sur Curry-Howard) qui échange les deux coordonnées d'un couple, et par lequel j'ai illustré la réalisabilité de cette formule. Donc mon exemple ci-dessus de la réalisabilité de A∧B⇒B∧A était juste une instance du théorème que je viens de citer.

En fait, et sans entrer dans les détails, le théorème ci-dessus ne dit pas juste que les formules intuitionnistement démontrables sont réalisables, mais même que la réalisabilité est close sous les règles de la logique intuitionniste : par exemple, si φ⇒ψ et φ sont réalisables, alors ψ aussi (c'est évident, il suffit d'appliquer le réalisateur de φ⇒ψ à celui de φ en utilisant la définition de ‘⇛’ ; et c'est ce que fait Curry-Howard).

Mentionnons aussi que si φ est réalisable, alors toute spécialisation de φ, i.e., toute formule obtenue en remplaçant chaque variable propositionnelle de φ par une formule propositionnelle quelconque, est encore réalisable.

Différence entre réalisabilité et typage

Si on a lu mon billet sur Curry-Howard, on peut avoir l'impression que je suis en train de réexpliquer les mêmes choses : en gros, voilà, si on a un théorème du calcul propositionnel intuitionniste, on le transforme en programme pour un langage de programmation typé (quelque chose comme : le λ-calcul simplement typé enrichi de types produits et sommes, 1 et 0), ce programme a un type qui correspond précisément à la formule démontrée, et ce programme fait exactement ce qu'on attend d'un « réalisateur » de la formule, ce qui n'est pas surprenant puisqu'on a défini les opérations ‘⊓’, ‘⊔’ et ‘⇛’ pour coller avec les constructions ‘×’, ‘+’ et ‘→’ (types produits, somme et fonction) sur les types, qui correspondent exactement aux connecteurs logiques ‘∧’, ‘∨’ et ‘⇒’. Est-ce que c'est la peine de raconter une nouvelle fois la même histoire ?

Et pourtant ! Voilà ce qui me surprend énormément, et qui devrait surprendre toute personne tentée de croire ce que j'ai résumé au paragraphe précédent (qui, tel que je l'ai écrit, n'est pas incorrect) : il existe des formules propositionnelles qui ne sont pas intuitionnistement démontrables et qui sont pourtant réalisables (je vais donner des exemples explicites ci-dessous, mais en voici déjà un : (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂))). En termes logiques, ça signifie qu'il n'y a pas complétude de la sémantique de la réalisabilité propositionnelle vis-à-vis du calcul propositionnel.

Maintenant, ceci est vrai : la correspondance de Curry-Howard nous dit effectivement qu'une formule intuitionnistement démontrable, c'est la même chose que le type d'un programme écrit dans le bon système (le λ-calcul simplement typé enrichi gnagnagna), et un tel programme réalise effectivement la formule en question.

Ce que ça sigifie que la formule (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂)) soit réalisable mais non démontrable, donc, c'est qu'il existe un programme (et je vais l'expliciter plus bas) qui réalise cette formule, en gros il prend en entrée des réalisateurs de ¬(A₁∧A₂) et (¬A₁⇒(B₁∨B₂)) et (¬A₂⇒(B₁∨B₂)) et en renvoie un de l'un de (¬A₁⇒B₁) ou (¬A₁⇒B₂) ou (¬A₂⇒B₁) ou (¬A₂⇒B₂) (remplacer ‘∧’, ‘∨’ et ‘⇒’ par ‘⊓’, ‘⊔’ et ‘⇛’ dans tout ça, si on veut, et réalisateur par élément) ; mais que ce programme n'est pas typable : il n'y a pas de programme de type (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂)) (remplacer ‘∧’, ‘∨’ et ‘⇒’ par ‘×’, ‘+’ et ‘→’ dans tout ça pour le comprendre comme un type).

Donc une façon de comprendre la morale de l'histoire, mais je ne sais pas si c'est la bonne, c'est que le typage (en tout cas le typage du λ-calcul simplement typé enrichi gnagnagna) restreint nos possibilités d'écrire des programmes qui font pourtant sens, même dans la mesure où ils retournent bien des choses moralement correctement typées : le programme qui réalise la formule (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂)), il renvoie au final bien des données correctement typées selon ce que cette formule indique, ce sont les manipulations intermédiaires qui échappent au typage et rendent le programme non typable.

Une autre façon de dire la même chose, c'est qu'il faut peut-être comprendre Curry-Howard comme une transformation des preuves en programmes non typés, c'est ça qui donne la réalisabilité des formules intuitionnistement démontrables, et ensuite on ajoute un typage côté programmes pour que cette transformation soit une correspondance bijective, i.e., qu'on n'appelle programmes correctement typés que ceux qui s'obtiennent de la sorte.

Je ne sais toujours pas bien quoi penser de cette histoire. Mais pour commencer, il faut regarder comment on fait pour réaliser une formule telle que (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂)) malgré le fait qu'elle ne soit pas intuitionnistement démontrable (i.e., pas le type d'un terme du λ-calcul simplement typé enrichi gnagnagna). Ce sera mon premier exemple.

La formule de Ceitin, et l'algorithme qui la réalise

Prenons l'exemple de la formule suivante, due à G. S. Ceitin (Г. С. Цейтин, parfois translittéré en Tseitin) :

(¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂)))
⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂))

(Je commence par cet exemple-là parce qu'il me semble que c'est le plus simple à comprendre.)

J'affirme que ⓐ elle n'est pas démontrable en calcul propositionnel intuitionniste, et que ⓑ pourtant, elle est réalisable.

Maintenant, expliquons ⓑ : pourquoi la formule de Ceitin est réalisable. C'est ça la partie intéressante de l'histoire. Et surtout, ça va être intéressant de chercher à regarder pourquoi et comment l'algorithme r qui va suivre n'est pas « typable ».

Mon but est donc de trouver un seul et même programme r qui la réalise, quelles que soient les parties P₁,P₂,Q₁,Q₂ de ℕ qu'on met à la place des variables A₁,A₂,B₁,B₂ de la formule. Autrement dit, ce programme attend une entrée dans ☇(P₁⊓P₂) ⊓ (☇P₁⇛(Q₁⊔Q₂)) ⊓ (☇P₂⇛(Q₁⊔Q₂)) et doit (sans avoir accès aux parties P₁,P₂,Q₁,Q₂) produire un résultat dans (☇P₁⇛Q₁) ⊔ (☇P₁⇛Q₂) ⊔ (☇P₂⇛Q₁) ⊔ (☇P₂⇛Q₂) où je rappelle que j'ai noté ☇R, parce que je manquais vraiment d'idée, l'ensemble R⇛∅ des promesses que R est vide.

En clair, notre algorithme reçoit en entrée

• une promesse que P₁ ou P₂ est vide (mais pas l'information de laquelle),
• un programme e₁ qui prend une promesse que P₁ est vide et renvoie soit un élément de Q₁ soit un élément de Q₂ (accompagné de la donnée du cas dans lequel on se trouve),
• un programme e₂ qui prend une promesse que P₂ est vide et renvoie idem,

et ce programme est censé renvoyer, pour certains i,j∈{1,2}, un programme prenant une promesse que P_i est vide et renvoyant un élément de Q_j, ainsi que la donnée du cas (i,j) qui a été choisi.

La difficulté dans l'histoire, c'est qu'on ne sait pas de façon évidente, justement, quel sera le « bon » choix : on a reçu la promesse que P₁ ou P₂ est vide, mais pas l'information de laquelle ; et dans chaque cas, on a reçu un programme e_i qui produit un élément de Q₁ ou de Q₂, ainsi que l'information du sous-cas où on se trouve, mais cette information sera garantie disponible seulement si la promesse en entrée est bonne (sinon, le programme e_i peut renvoyer n'importe quoi, ou ne pas terminer du tout), et avec tout ça il faut quand même arriver à choisir (i,j) pour lesquels on fournit un élément de ☇P_i⇛Q_j.

Voici comment fait notre algorithme. Il lance en parallèle l'exécution de e₁ et e₂, en leur fournissant une entrée quelconque (mettons 42, si on veut) : ceci est possiblement une « fausse promesse », c'est-à-dire qu'on ne sait pas si P₁ est vide, ni si P₂ est vide, on est en train de promettre le premier fait à e₁ et le second fait à e₂, mais on ne sait pas quelle est la vérité. On sait cependant, d'après le premier point de l'entrée, que l'un de P₁ ou P₂ est vide. c'est-à-dire que l'une (au moins) des deux promesses qu'on a faites est vraie (comme une promesse n'a pas de contenu informatif, sa valeur n'a pas d'importance, la seule chose qui compte est qu'elle soit vraie ou pas). Donc soit e₁ terminera soit e₂ terminera (sur la valeur qu'on leur a fournie) et renverra une valeur de la forme ⟨k,s⟩ avec k∈{0,1} et s∈ℕ (s'il renvoie une valeur d'une autre sorte, on l'ignore et on attend que l'autre termine). Par symétrie, mettons sans perte de généralité que e₁ termine et renvoie une valeur comme on l'a dit.

Notez que la valeur ⟨k,s⟩ n'est pas forcément dans Q₁⊔Q₂ pour autant, parce que même si e₁ a terminé, ce n'est pas pour autant qu'il a reçu une vraie promesse (un élément de R⇛S qui reçoit un élément qui n'est pas dans R a le droit de renvoyer n'importe quoi, ou de ne pas renvoyer du tout). Mais ce n'est pas grave. Mettons sans perte de généralité que k=0, c'est-à-dire que e₁ semble prétendre que s appartient à Q₁ (désolé pour ce décalage de 1…), et, de fait, c'est le cas si la promesse en entrée était vraie.

On renvoie alors le programme q suivant, annoncé comme étant dans ☇P₁⇛Q₁ : le programme prend en entrée une promesse t que P₁ est vide, et renvoie la valeur s.

Ce programme q fait bien ce qu'il est censé faire : en effet, si t est une vraie promesse, c'est-à-dire si P₁ est vraiment vide, c'est que e₁ a reçu une vraie promesse en entrée (car, justement, P₁ est vide, et que toutes les promesses sont interchangeables), donc en terminant il a dû renvoyer un élément ⟨k,s⟩ de Q₁⊔Q₂, donc (comme on est dans le cas k=0), on a bien s∈Q₁. Bref, on a bien renvoyé un élément de ☇P₁⇛Q₁.

Et du coup, l'ensemble de l'algorithme r réalise la formule de Ceitin.

Pour récapituler, voici mon algorithme r complet réalisant la formule de Ceitin, où je parenthèse le deuxième membre comme ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂)) ∨ ((¬A₂⇒B₁) ∨ (¬A₂⇒B₂)) (ça ne change rien mais ça ce sera plus clair pour les notations) : r prend en entrée ⟨n,e₁,e₂⟩, il lance en parallèle l'exécution de e₁ sur 42 et de e₂ sur 42, et il attend que l'un d'eux termine avec une valeur de la forme ⟨k,s⟩ pour k∈{0,1} ; il renvoie alors ⟨0,⟨k,q_s⟩⟩ si c'est e₁ qui a fourni la valeur ou ⟨1,⟨k,q_s⟩⟩ si c'est e₂ qui l'a fournie, où q_s est un programme qui ignore la valeur t passée en argument et renvoie toujours s.

*

Je répète qu'on ne peut pas trouver de programme typé (dans le cadre du λ-calcul simplement typé enrichi de types produits et sommes, 1 et 0) qui réalise l'algorithme ci-dessus, ou même simplement qui ait le type qui correspond à la formule de Ceitin. Il est intéressant de prendre note de ce qu'a fait l'algorithme ci-dessus qui dépasse les possibilités du typage :

• lancer deux programmes en parallèle, sachant (par une preuve donnée par ailleurs) qu'au moins l'un des deux doit terminer et renvoyer un résultat correct,
• créer une possiblement « fausse promesse », sachant (par une preuve donnée par ailleurs) qu'au moins l'une des deux qu'on a créées est vraie.

La formule de Rose (et sa transformation en énigme avec un snark)

La formule qui suit est la première qui a été découverte qui soit réalisable mais non démontrable (par G. F. Rose en 1953). Elle est la suivante :

((¬¬D⇒D) ⇒ (D∨¬D)) ⇒ (¬¬D∨¬D)
où D := (¬A ∨ ¬B)

autrement dit, elle s'obtient en substituant (¬A ∨ ¬B) à la place de la variable D dans la formule, dite formule de Scott, ((¬¬D⇒D) ⇒ (D∨¬D)) ⇒ (¬¬D∨¬D). Je reparlerai plus bas de cette formule de Scott, pour dire que, toute seule, elle n'est pas réalisable, et en particulier pas démontrable, mais je peux d'ores et déjà noter deux choses à son sujet. D'abord, elle est (démontrablement) équivalente à ((¬¬D⇒D) ⇒ (¬¬D∨¬D)) ⇒ (¬¬D∨¬D) (lorsque D est une variable, donc a fortiori lorsque D est substituée) donc on peut préférer écrire ça ; d'autre part, cette formule de Scott est située autour de la 10e position (selon comment on compte) dans le treillis de Rieger-Nishimura qui répertorie toutes les formules propositionnelles en une seule variable modulo équivalence intuitionnistement démontrable, donc c'est assez naturel de considérer précisément cette chose-là.

Je ne vais pas démontrer que la formule de Rose n'est pas démontrable, ce n'est pas très dur mais pas terriblement intéressant. (De toute façon il existe un algorithme pour savoir si une formule propositionnelle est intuitionnistement démontrable — consistant à rechercher ce qu'on appelle une démonstration sans coupure, ce qui rend la recherche exhaustive finie — qui est par exemple implémenté dans Coq sous le nom de la tactique tauto, donc on peut simplement entrer la formule dans Coq et lui demander de vérifier.)

Mais expliquons pourquoi elle est réalisable, et ce que ça nous apprend qu'elle le soit.

Il faut donc imaginer qu'on a deux variables A,B représentées par des parties de ℕ (auxquelles, on rappelle, l'algorithme qu'on va construire n'aura pas accès), mais comme elles apparaissent dans la formule uniquement par le truchement de ¬A et ¬B, seule nous intéresse ici la question de savoir si elles sont habitées ou vide. (On peut considérer ça comme des « booléens cachés ».) Plus exactement, seule nous intéresse la question, représentée par la variable D, de décider si l'une des parties A ou B est vide. Autrement dit, il faut imaginer que D représente l'information (au moins) une des deux parties est vide et je sais précisément laquelle, ¬D représente les deux sont habitées, et ¬¬D représente (au moins) une des deux parties est vide, sans information sur laquelle. La disjonction (¬¬D∨¬D) se lit donc comme la capacité à décider si oui ou non une des deux parties est vide ; quant à (¬¬D⇒D), elle représente un programme qui, si on a la promesse qu'une des deux parties est vide, va déterminer laquelle.

Je peux transformer ça en une énigme, si je veux : il y a devant moi deux portes, A et B. Peut-être qu'il y a un snark derrière l'une ou l'autre ou les deux de ces deux portes (je vais prendre le « snark » comme représentant ¬A ou ¬B, i.e., la partie est vide, parce que c'est ça qui apparaît plus naturel). Mon but (décrit par ¬¬D∨¬D) est de déterminer s'il y a un snark derrière l'une des deux portes (mais pas forcément de dire quelle porte). Pour ça, je dispose comme indice d'un programme p (décrit par (¬¬D⇒D) ⇒ (¬¬D∨¬D)) qui va justement répondre à cette question, mais à condition que je lui passe en entrée un programme q (décrit par ¬¬D⇒D) qui, s'il y a un snark, indique une porte où il y en a un. Comment est-ce que je fais ?

Solution de l'énigme : en fait, c'est vraiment facile : pour chasser le snark, il suffit d'envoyer quelqu'un chasser le snark derrière la porte A et quelqu'un chasser le snark derrière la porte B. C'est-à-dire que je lance en parallèle mon programme-indice p sur deux entrées différentes : l'une q_A renvoie toujours A (i.e., promet que s'il y a un snark il y en a un en A) et l'autre q_B renvoie toujours B (i.e., promet que s'il y a un snark il y en a un en B). S'il n'y a pas de snark, les deux q_A et q_B remplissent bien la contrainte demandée, donc les deux copies de p vont toutes les deux répondre il n'y a pas de snark ; en revanche, s'il y a un snark, disons en A, alors q_A remplit bien la contrainte demandée, donc la copie de p qui a reçu q_A en entrée va répondre il y a un snark (l'autre pourrait faire n'importe quoi : ne pas terminer, répondre qu'il y a un snark, ou qu'il n'y en a pas, ou répondre 42). Bref, j'attends que soit les deux copies de p lancées en parallèle répondent il n'y a pas de snark soit que l'une d'elles réponde il y a un snark : dans le premier cas je réponds il n'y a pas de snark et dans le second il y a un snark.

Noter que je sais, au final, s'il y a un snark, mais pas forcément où il est : parce que même si la copie de p qui a reçu q_A en entrée a répondu il y a un snark, il se pourrait quand même que le snark soit en B et que ce soit une réponse arbitraire de p qui a reçu une fausse promesse q_A en entrée (mais il y a forcément un snark, parce que s'il n'y en avait pas, q_A remplirait la contrainte et la réponse serait obligatoirement il n'y a pas de snark).

Maintenant, si on veut, je transforme ça en algorithme qui réalise la formule de Rose : il faut juste arrêter de parler de snark en A/B et dire la partie A/B est vide. Ceci donne l'algorithme suivant :

Mon programme r prend en entrée un programme p censé appartenir à (☇☇D⇛D) ⇛ (D⊔☇D). Je prépare deux programmes q_A et q_B : le premier ignore son entrée et renvoie ⟨0,0⟩ (ce qui est censé appartenir à D := ☇A⊔☇B si A est vide), tandis que le second ignore son entrée et renvoie ⟨1,0⟩ (ce qui est censé appartenir à D := ☇A⊔☇B si B est vide). Je lance en parallèle p sur les entrées q_A et q_B, et j'attends que soit les deux terminent en renvoyant quelque chose de la forme ⟨1,—⟩, soit que l'un d'eux termine en renvoyant quelque chose de la forme ⟨0,—⟩. Dans le premier cas, je (i.e., mon algorithme r) renvoie ⟨1,0⟩, dans le second je renvoie ⟨0,0⟩.

Quelques autres formules réalisables et non démontrables

La formule assez compliquée qui suit est due à Plisko :

((¬¬A⇔(¬B∧¬C)) ∧ (¬¬B⇔(¬C∧¬A)) ∧ (¬¬C⇔(¬A∧¬B))
∧ ((¬A⇒(¬B∨¬C)) ⇒ (¬B∨¬C)) ∧ ((¬B⇒(¬C∨¬A)) ⇒ (¬C∨¬A)) ∧ ((¬C⇒(¬A∨¬B)) ⇒ (¬A∨¬B)))
⇒ (¬A ∨ ¬B ∨ ¬C)

(Noter qu'il y a une typo dans la manière dont elle est écrite à plusieurs endroits, notamment dans le survey de Plisko lui-même, ce qui n'aide pas à suivre. La formule correcte est complètement symétrique en A,B,C.)

Si on traduit la partie [associée à la variable] A/B/C est habitée par la porte A/B/C a un dragon derrière, alors en traduisant la recherche d'un réalisateur de cette formule on obtient exactement[#5] l'énigme que j'avais proposée ici. (On a trois « booléens cachés », ¬¬A,¬¬B,¬¬C, on reçoit la promesse qu'un seul des trois est vrai, et trois « indices », et le but est de déterminer un booléen faux ; les indices renvoient chacun un booléen faux parmi une paire de deux d'entre eux, mais à condition soit que le troisième booléen soit vrai soit qu'on ait passé un argument qui fait précisément ça.)

[#5] C'est exactement ça qui s'est passé : j'ai voulu comprendre pourquoi cette formule était réalisable, j'ai traduit ça en une énigme pour essayer de mieux visualiser ce qui se passait et pour m'aider à réfléchir dessus, et j'ai écrit cette énigme dans ce blog.

Je ne recopie donc pas la solution de l'énigme, mais la formule est bien réalisable. Comme les formules de Ceitin et de Rose, elle n'est pas intuitionnistement démontrable. Ce qui la rend intéressante, c'est qu'ici, non seulement elle n'est pas démontrable, mais elle n'est même pas valide au sens des problèmes finis de Medvedev, ce qui reflète essentiellement le fait que l'énigme n'est pas résoluble si on remplace des programmes par des tableaux (j'avais écrit la définition de la logique des problèmes finis de Medvedev dans un bout de ce billet par ailleurs fort mal écrit, mais disons pour résumer que c'est grosso modo pareil que la réalisabilité sauf qu'on travaille sur des ensembles finis non spécifiés avec des fonctions quelconques au lieu de travailler sur ℕ avec la calculabilité[#6]).

[#6] Pour les gens qui savent ce que ça veut dire, la logique des problèmes finis de Medvedev est la logique (propositionnelle) interne du topos des ensembles simpliciaux, comme expliqué ici par Emil Jeřábek sur MathOverflow, de la même manière que la réalisabilité propositionnelle est la logique (propositionnelle) interne du topos effectif (et que la sémantique des ouverts est la logique (propositionnelle) interne du topos de faisceaux sur un espace topologique).

*

La formule suivante est due à V. A. Ânkov (В. А. Янков, diversement translittéré en Yankov ou Jankov, voire Jankow) :

(¬(A∧B) ∧ ¬(¬A∧¬B) ∧ ((¬¬A⇒A)⇒(A∨¬A)) ∧ ((¬¬B⇒B)⇒(B∨¬B))) ⇒ (¬A∨¬B)

De nouveau, elle n'est pas intuitionnistement démontrable.

Voici comment on peut la réaliser. Il y a deux parties A,B⊆ℕ auxquelles je n'ai pas accès (je me permets maintenant de noter les parties comme les variables parce que c'est pénible à ce stade de systématiquement changer mes A,B en P,Q pour rien). Je reçois une promesse que l'une et exactement l'une de ces parties est habitée, ainsi que, pour chacune d'elles, un programme (appelons-les p_A et p_B, lesquels appartiennent à (☇☇A⇛A)⇛(A⊔☇A) et (☇☇B⇛B)⇛(B⊔☇B) respectivement) qui va dire si elle est habitée à condition qu'il reçoive en entrée un autre programme q donnant un « élément potentiel » de la partie (c'est-à-dire un programme qui, si la partie est habitée, renvoie un élément qui y appartienne) ; et mon but est de dire quelle partie est vide. Ce que je vais faire est parcourir tous les entiers naturels n en parallèle (c'est-à-dire en utilisant un déployeur universel) et, pour chacun, lancer p_A et p_B sur un programme q_n qui juste renvoie n, jusqu'à trouver un n pour lequel l'un des deux programmes p appelé sur q_n me dise que sa partie est habitée et que l'autre me dise qu'elle est vide. Comme l'une des deux parties est habitée, mettons sans perte de généralité que A le soit, il va y avoir un n qui appartient à A, et pour ce n le programme q_n appartient à la fois à ☇☇A⇛A (puisqu'il renvoie n) et ☇☇B⇛B (car c'est ℕ tout entier), donc la condition que j'attends sera bien vérifiée et ma recherche terminera. Et comme une des parties est vide, mettons que B le soit, je ne peux jamais avoir de fausse réponse (tout q appartient à ☇☇B⇛B), donc j'aurai toujours une bonne réponse d'un côté même si la promesse de l'autre côté est fausse.

*

Mon dernier exemple de formule réalisable mais non démontrable est de nouveau du à Plisko :

(¬(A∧B) ∧ ¬(¬C₁∧¬C₂) ∧ (((A⇒C₁) ∨ (A⇒C₂)) ⇒ ((B⇒C₁) ∨ (B⇒C₂)))) ⇒ ((B⇒C₁) ∨ (B⇒C₂))

Voici comment on peut la réaliser. De nouveau, j'appelle par les mêmes lettres A,B,C₁,C₂ les parties de ℕ (auxquelles je n'ai pas accès) mises pour les variables de cette formule. L'algorithme r que je vais construire reçoit une promesse que A et B ne sont pas tous les deux habités, une promesse que C₁ et C₂ ne sont pas tous les deux vides, et un programme p prenant en entrée soit un programme envoyant A dans C₁ soit un programme renvoyant A dans C₂ (avec l'information duquel on a donné) renvoyant en sortie soit un programme envoyant B dans C₁ soit un programme renvoyant B dans C₂ (avec l'information duquel a été renvoyé) ; et il (r) doit renvoyer soit un programme envoyant B dans C₁ soit un programme renvoyant B dans C₂ (avec l'information duquel a été renvoyé). Pour ça, on parcourt les entiers naturels n en parallèle (comme dans la formule précédente) et, pour chacun, on appelle q_n le programme qui juste renvoie n et on lance en parallèle p sur ⟨0,q_n⟩ et sur ⟨1,q_n⟩, autrement dit, en prétendant que q_n envoie A dans C₁ et en prétendant que q_n envoie A dans C₂, et ce, jusqu'à tomber sur un n et un i∈{0,1} pour lesquels p termine sur ⟨i,q_n⟩ en renvoyant une valeur de la forme ⟨j,s⟩ avec j∈{0,1} ; alors on renvoie simplement cette valeur ⟨j,s⟩ que p aura renvoyée. Comme on a reçu la promesse que C₁ et C₂ ne sont pas tous les deux vides, on va finir par tomber sur un n qui est dans C₁ ou dans C₂, donc q_n (qui implémente juste la fonction constante de valeur n) est dans A⇛C₁ ou A⇛C₂, donc p finit par renvoyer quelque chose de la forme ⟨j,s⟩. Si A est vide, tous les ⟨i,q_n⟩ sont dans (A⇛C₁) ⊔ (A⇛C₂), donc la valeur renvoyée par p est garantie correcte et on a rempli le contrat ; si B est vide, n'importe quel ⟨j,s⟩ est dans (B⇛C₁) ⊔ (B⇛C₂) donc on a aussi rempli le contrat. Donc dans tous les cas, la valeur renvoyée par notre algorithme r est correcte.

Y a-t-il un truc général ?

J'ai donné cinq ou six exemples de formules réalisables mais non démontrables (une de Ceitin, plus une variante plus générale proposée par Skvorcov, une de Rose, deux de Plisko et une de Ânkov).

On peut trouver d'autres exemples[#7], mais il n'y en a pas des masses de connues qui soient substantiellement différentes. En fait, j'ai essentiellement fait le tour : Skvorcov a vérifié en 1995 que toutes les formules connues à l'époque (et je ne crois pas qu'il y en ait de nouvelle qui soit sortie depuis) se déduisaient de la version un peu plus générale de la formule de Ceitin, et des trois formules (deux de Plisko et une de Ânkov) que j'ai données dans la section précédente.

[#7] Celle-ci, que je laisse en exercice, est assez jolie, et possiblement instructive : (¬(A∧B) ∧ ¬(B∧C) ∧ ¬(C∧A) ∧ (¬C ⇒ A∨B) ∧ (¬A ⇒ B∨C) ∧ (¬B ⇒ C∨A)) ⇒ A∨B∨C (comme la formule de Rose, elle découle de celle de Ceitin, mais en même temps elle ressemble à celle de Plisko que j'ai utilisée pour mon énigme de dragon).

Donc la difficulté à trouver des formules réalisables non démontrables n'est pas tant de vérifier qu'elles ne sont pas démontrables, ni même de vérifier qu'elles sont réalisables — c'est de trouver ces formules. Pour vérifier qu'elles sont réalisables, c'est un petit jeu d'énigme, amusant et pas très difficile (je n'ai pas lu les preuves dans la littérature, j'ai retrouvé tout ça moi-même), mais c'est comme les casse-tête : les gens qui m'impressionnent ne sont pas ceux qui les résolvent mais ceux qui les conçoivent.

Et manifestement, on n'a pas de méthode générale pour produire des formules réalisables non démontrables.

En fait, on ignore quasiment tout à ce sujet : si j'ai bien compris, on ignore si l'ensemble des formules propositionnelles réalisables est décidable, ou même semi-décidable ou de complémentaire semi-décidable. (Pour les formules propositionnelles démontrables, en revanche, je l'ai déjà dit mais je le redis pour mémoire, il y a bien un algorithme.)

Il y a quand même une chose importante qu'on sait, c'est que toute formule écrite sans le ‘⊥’ (et donc, en particulier, sans ‘¬’) qui est réalisable est en fait démontrable. (Ce résultat a été prouvé avec une erreur par Medvedev en 1963 ; l'erreur a été corrigée par Plisko en 1973, mais la preuve n'a apparemment été publiée qu'en 2002.) Je vais brièvement revenir sur la question dans la conclusion.

Formules non réalisables pour des raisons « triviales » d'information

Trouver des formules non réalisables est, contrairement aux réalisables non (intuitionnistement) démontrables, très facile, même si on se restreint à celles qui sont au moins classiquement démontrables (on a vu que c'était nécessaire). L'argument de leur non-réalisabilité va souvent être quelque chose comme évidemment que sans avoir accès aux parties de ℕ on ne peut pas produire un élément de ce truc. Par exemple, la formule (¬(A∧B) ∧ ¬(B∧C) ∧ ¬(C∧A)) ⇒ (¬A ∨ ¬B ∨ ¬C) n'est pas réalisable parce c'est évident que, parmi trois parties de ℕ, même si on a la promesse qu'au plus une des trois est habitée, on ne peut pas en produire une qui soit vide (une preuve précise va consister à considérer les trois possibilités (ℕ,∅,∅), (∅,ℕ,∅) et (∅,∅,ℕ) pour les trois parties, et constater qu'aucun choix entre ¬A, ¬B et ¬C ne peut convenir pour les trois ; mais ce que je souligne c'est à quel point c'est évident).

Voici un autre exemple, un petit peu moins évident, mais toujours très facile, que je rédige complètement pour pouvoir comparer avec la suite : j'affirme que la formule (C⇒(B₁∨B₂)) ⇒ ((C⇒B₁) ∨ (C⇒B₂)) n'est pas réalisable. En effet, supposons par l'absurde que r la réalise. C'est-à-dire que r doit appartenir à (C⇛(B₁⊔B₂)) ⇛ ((C⇛B₁) ⊔ (C⇛B₂)) pour toutes parties B₁,B₂,C de ℕ. En particulier, c'est le cas pour C = (B₁⊔B₂), ce que je choisis maintenant de prendre. Cette hypothèse assure que si p est un programme qui calcule la fonction identité, alors p est dans C⇛(B₁⊔B₂). Donc je peux lancer r avec p comme entrée, et il doit terminer et du coup renvoyer un résultat de la forme ⟨0,s⟩ (assurant que s est dans C⇛B₁) ou bien ⟨1,s⟩ (assurant que s est dans C⇛B₂). Supposons sans perte de généralité qu'on soit dans le premier cas. Alors je prends pour B₁ l'ensemble vide ∅, pour B₂ l'ensemble plein ℕ (et pour C l'ensemble ∅⊔ℕ). On devrait avoir s dans C⇛B₁, ce qui est impossible car C⇛B₁ est vide (puisque B₁ est vide mais C ne l'est pas).

L'argument que je viens de donner pour montrer que (C⇒(B₁∨B₂)) ⇒ ((C⇒B₁) ∨ (C⇒B₂)) n'est pas réalisable ne dépend de rien de particulier sur les machines de Turing ou la calculabilité. On pourrait dire que c'est un argument de pure « théorie de l'information » (complètement trivial(e)), pas de calculabilité : comme le programme r n'a pas accès aux parties mises pour B₁,B₂,C, il ne peut pas réaliser la formule proposée, parce qu'il n'a tout simplement pas l'information nécessaire.

Je ne sais pas bien comment formaliser cette idée que certaines formules ne sont pas réalisables pour des raisons « idiotes » de manque d'information. Un élément pertinent est que la formule que je viens de donner n'est pas valable au sens des problèmes finis de Medvedev (brièvement évoquée plus haut), avec essentiellement la preuve que je viens de donner, alors que les deux exemples « non-idiots » que je vais exposer ci-dessous (les formules de Kreisel-Putnam et Scott) ne le sont pas. Mais je ne sais pas si c'est vraiment ça qui importe : après tout, j'ai donné un exemple plus haut de formule qui est réalisable et n'est pas valable au sens des problèmes finis. Donc il y a clairement quelque chose qui m'échappe, ici.

Quoi qu'il en soit, je veux donner deux exemples de formules qui ne sont pas réalisables, mais qui le sont pour des raisons qui semblent être non « idiotes ». Ces deux formules ont un intérêt logique à divers titres (elles sont valables au sens des problèmes finis de Medvedev, et elles définissent — séparément ou bien jointement — des logiques qui sont décidables et ont la propriété de la disjonction), mais à la limite, peu importe.

La formule de Kreisel-Putnam

La formule de Kreisel-Putnam (ou axiome de Kreisel-Putnam pour des raisons historiques) est la suivante :

(¬A⇒(B₁∨B₂)) ⇒ ((¬A⇒B₁) ∨ (¬A⇒B₂))

Informellement parlant, réaliser cette formule, ce serait « devancer un choix sous promesse » : on a un programme qui doit choisir entre renvoyer des éléments de B₁ et B₂ sous la promesse que quelque chose est vérifié (que A soit vide, peu importe), et on doit transformer ça (algorithmiquement, donc !) en un choix entre un programme qui renvoie un élément de B₁ et un programme qui renvoie un élément de B₂, toujours sous la même promesse, mais le choix entre les deux cas doit être effectué avant d'avoir reçu la promesse, et c'est ça qui va être impossible — mais « presque » possible — et rendre la formule de Kreisel-Putnam intéressante.

Je vais montrer qu'elle n'est pas réalisable, mais commençons par expliquer pourquoi on peut « presque » la réaliser.

Un réalisateur r de cette formule reçoit en entrée un programme p qui, sous une certaine promesse (que A est vide, mais peu importe, c'est juste une certaine promesse) renverra soit un élément de B₁ soit un élément de B₂ ; le programme r est censé transformer p en soit un programme qui (toujours sous la même promesse) renvoie un élément de B₁ soit un programme qui (toujours sous la même promesse) renvoie un élément de B₂. Cette fois, il n'y a pas d'obstacle d'information à faire ça. En effet, si on disposait d'un accès à l'oracle de l'arrêt des machines de Turing, par exemple, on pourrait très bien considérer ce qui se passe si on lance p sur l'entrée 0 (les promesses sont toutes interchangeables, donc peu importe la valeur), utiliser l'oracle pour décider s'il s'arrête ou pas : s'il s'arrête, on l'exécute on calcule ce qu'il renvoie et, si c'est de la forme ⟨i,t⟩ avec i∈{0,1}, on renvoie ⟨i,q_t⟩ où q_t est la fonction constante de valeur t ; tandis que si p ne termine pas (ce qui ne peut se produire que lorsque A est habité), on renvoie ⟨0,0⟩. Ceci fournit bien un élément de de (☇A⇛B₁) ⊔ (☇A⇛B₂) en fonction d'un élément de ☇A⇛(B₁⊔B₂) : le seul problème est que calculer cette « fonction » nécessite l'accès à l'oracle de l'arrêt[#8]. Mais le fait que ce soit possible comme ça montre que le problème à réaliser la formule de Kreisel-Putnam est bien plus subtil que pour les exemples « idiots » de la section précédente : l'information nécessaire est bien là, ce qui manque c'est la puissance de calcul pour l'exploiter.

[#8] En fait, ce que montre le paragraphe précédent, c'est que la formule ((¬A⇒(B₁∨B₂)) ⇒ ○((¬A⇒B₁) ∨ (¬A⇒B₂))) est réalisable, où ‘○’ est ici un modalisateur devant être interprété comme le saut de Turing, c'est-à-dire qu'on définit ⟦○φ⟧ comme l'ensemble des programmes pour machines de Turing ayant accès à l'oracle de l'arrêt et qui calculent un résultat dans ⟦φ⟧. Plus généralement, chacun des oracles au sens expliqué dans ce billet définit très naturellement un modalisateur (comme, pour ceux qui savent ce que ça veut dire, n'importe quelle topologie de Lawvere-Tierney sur un topos) et on peut s'interroger sur la réalisabilité de formules propositionnelles modales impliquant divers de ces modalisateurs. (Je ferai des remarques vaseuses à ce sujet à la fin.)

Je souligne que j'ai expliqué plus haut que (C⇒(B₁∨B₂)) ⇒ ((C⇒B₁) ∨ (C⇒B₂)) (c'est-à-dire la formule plus générale avec C à la place de ¬A dans la formule de Kreisel-Putnam) n'est pas réalisable pour des raisons beaucoup plus triviales (ce n'est pas un saut de Turing qui vous sauvera, là !) : ce qui rend la formule de Kreisel-Putnam « presque » réalisable, et donc plus intéressante, c'est qu'on cherche juste à retarder la réception d'une promesse, or une promesse n'a pas de contenu informatif, donc on est à deux doigts (en l'occurrence, à un saut de Turing) près de pouvoir la réaliser. (Mais pour que ça marche, on a quand même besoin de la promesse pour assurer que le programme terminera.)

Maintenant, montrons que la formule de Kreisel-Putnam n'est pas réalisable (sans la triche consistant à invoquer l'oracle de l'arrêt, donc).

Pour ça, j'invoque et rappelle le fait classique de calculabilité qu'on peut fabriquer des parties semi-décidables et calculablement inséparables : c'est-à-dire deux parties W₁ et W₂ de ℕ, disjointes, telles qu'on puisse algorithmiquement énumérer les éléments de W₁ comme ceux de W₂ (i.e., elles sont semi-décidables), mais qu'il n'existe pas d'algorithme qui, donné un élément n de ℕ, termine toujours en temps fini et renvoie 1 lorsque n∈W₁ et 2 lorsque n∈W₂ (et si n n'est dans ni l'un ni l'autre, il peut renvoyer n'importe quoi, mais il doit quand même terminer en temps fini, c'est bien ça le point crucial). Un exemple de tels ensembles (que j'avais mentionné ici) est d'appeler W₁ l'ensemble des théorèmes de (disons) l'arithmétique de Peano, et W₂ l'ensemble des négations de théorèmes. Un autre exemple, peut-être plus simple, consiste à appeler W₁ l'ensemble des programmes qui (sur une entrée triviale) terminent et renvoient 1 et W₂ l'ensemble de ceux qui terminent et renvoient 2. (Voir aussi cette question et la réponse que j'y ai faite pour une discussion sur les degrés possibles de tels ensembles.)

Supposons maintenant par l'absurde que r réalise la formule de Kreisel-Putnam. Je vais montrer que je peux m'en servir pour séparer calculablement W₁ et W₂, i.e., je vais produire un algorithme qui, donné n, termine toujours en temps fini et renvoie 1 ou 2 selon que n∈W₁ ou n∈W₂, ce qui est justement impossible. Pour ça, j'applique r au programme p qui, donné une entrée qui sera ignorée, énumère W₁ et W₂ en parallèle jusqu'à peut-être trouver l'élément n dans l'un des deux : s'il le trouve dans W₁, il [c'est-à-dire, p] termine et renvoie ⟨0,q_n⟩ où q_n est la fonction constante de valeur n, et s'il le trouve dans W₂, il termine et renvoie ⟨1,q_n⟩ où q_n est la fonction constante de valeur n. On notera que p ne termine pas forcément. Néanmoins, je vais montrer que r va forcément terminer quand on l'applique à p, et de plus, renvoyer un résultat de la forme ⟨0,—⟩ ou ⟨1,—⟩, qui sera forcément de la forme ⟨0,—⟩ si n∈W₁, et de la forme ⟨1,—⟩ si n∈W₂, ce qui me permet de finir mon algorithme en renvoyant 1 dans le premier cas et 2 dans le second (encore une fois, désolé pour ce décalage de 1). Pour montrer que cet algorithme marche bien, il y a trois cas à distinguer (noter qu'algorithmiquement je ne sais pas dans quel cas je suis, mais ce n'est pas grave, je peux quand même raisonner dans chacun et faire des définitions) :

• Si n∈W₁, alors posons B₁=ℕ et A=B₂=∅. Alors p appartient à ☇A⇛(B₁⊔B₂) puisqu'il termine et renvoie ⟨0,—⟩ (peu importe la seconde valeur). Donc r appliqué à p termine et renvoie le codage d'un couple appartenant à (☇A⇛B₁ ⊔ (☇A⇛B₂). Comme B₂ est vide et que ☇A ne l'est pas, rien l'ensemble ☇A⇛B₂ est vide, donc le couple renvoyé par r est forcément de la forme ⟨0,—⟩, et mon algorithme final a correctement renvoyé 1.
• Si n∈W₂, alors posons B₂=ℕ et A=B₁=∅ et tout est symétrique au cas précédent.
• Enfin, si n n'est ni dans W₁ ni dans W₂, on pose A=ℕ et B₁=B₂=∅. Alors le fait que A soit habité (donc que ☇A soit vide) assure que tout entier naturel, et certainement notre programme p (même s'il ne termine pas) appartient à ☇A⇛(B₁⊔B₂), donc r doit quand même terminer quand on l'applique à p, et renvoyer le codage d'un couple dans (☇A⇛B₁) ⊔ (☇A⇛B₂), donc quelque chose de la forme ⟨0,—⟩ ou ⟨1,—⟩, peu importe, mais en tout cas il doit terminer, ce qui assure que mon algorithme termine bien dans ce cas aussi,

Bref, dans tous les cas mon algorithme termine, et il sépare W₁ et W₂, ce qui n'était pas possible. D'où la contradiction : le programme r ne peut pas exister, et la formule de Kreisel-Putnam n'est pas réalisable.

La formule de Scott

La formule de Scott (ou axiome de Scott) est la suivante :

((¬¬D⇒D) ⇒ (D∨¬D)) ⇒ (¬¬D∨¬D)

On l'a déjà rencontrée comme squelette de la formule de Rose (qui est bien réalisable), où D était remplacé par (¬A ∨ ¬B), mais cette fois-ci on va laisser D comme variable propositionnelle. Si on préfère, on peut la remplacer par la version (intuitionnistement démontrablement) équivalente suivante :

((¬¬D⇒D) ⇒ (¬¬D∨¬D)) ⇒ (¬¬D∨¬D)

(En effet, (¬¬D⇒D) ⇒ (¬¬D∨¬D) implique (¬¬D⇒D) ⇒ (D∨¬D) puisque sous l'hypothèse on peut justement remplacer ¬¬D par D ; et la réciproque est évidente car D implique de toute façon ¬¬D.)

Informellement parlant, réaliser cette formule, ce serait arriver à décider si une partie D est habitée ou vide en ayant accès à un programme qui peut répondre à cette question à condition qu'on lui fournisse en entrée un élément potentiel de D (un élément potentiel désignant, ici, un élément qui appartient à D si D est habité).

De nouveau, on peut en un sens « presque » la réaliser.

Comment ? Supposons qu'on me fournisse un programme p qui soit dans (☇☇D⇛D) ⇛ (☇☇D⊔☇D) (ou (☇☇D⇛D) ⇛ (D⊔☇D), peu importe). Je peux imaginer appeler p sur le programme q_n qui renvoie constamment n : si n est dans D ou bien que D est vide, alors q_n appartient à ☇☇D⇛D, donc p va répondre correctement sur ce q_n. Si j'avais accès à deux niveaux d'oracle de l'arrêt (je veux dire, à 0″), je pourrais faire la chose suivante : (en utilisant le premier niveau d'oracle de l'arrêt 0′) décider pour chaque n si p appelé avec q_n termine et le cas échéant calculer sa réponse, puis (en utilisant le deuxième niveau) décider si tous ces appels renvoient la branche de la disjonction : si tous renvoient la même chose, cette réponse est correcte et je peux la renvoyer ; et si l'un renvoie quelque chose de différent, je sais que D est habité et je renvoie ce fait (c'est-à-dire que je renvoie ⟨0,0⟩ qui appartient à ☇☇D⊔☇D). Ça marche, mais, de nouveau, j'ai eu besoin de sauts de Turing (deux cette fois, mais je ne sais pas si c'est vraiment significatif).

Maintenant, expliquons pourquoi la formule de Scott n'est pas réalisable (sans la triche consistant à invoquer d'oracles donc). En fait, la recherche de choix de D rendant irréalisable cette formule correspond à l'énigme que j'avais proposée ici, mais comme ce n'est pas forcément super clair quel est le rapport, je vais le redire indépendamment ici. (L'argument qui suit est dû à Ânkov pour son essence, mais je l'ai retraduit à ma sauce ; voyez ici pour des détails de comment il l'a écrit.)

Supposons par l'absurde que r réalise la formule de Scott. Je vais montrer que je peux m'en servir pour décider l'oracle de l'arrêt, i.e., je vais produire un algorithme qui, donné n, termine toujours en temps fini et renvoie oui ou non selon que le programme (codé par l'entier) n termine en temps fini ou non. Si le programme codé par n termine en temps fini, appelons b(n) le nombre d'étapes de son exécution, et appelons h(n) = B(b(n)) où B(N) est le maximum plus un parmi les valeurs bien définies renvoyées par les N premiers programmes quand on les exécute avec l'entrée 0. On pose enfin D_n l'ensemble des entiers naturels ≥h(n). En revanche, si le programme codé par n ne termine pas en temps fini, on pose D_n = ∅. Maintenant, si q appartient à ☇☇D_n⇛D_n et que le programme codé par n termine en temps fini, alors q appelé sur 0 renvoie un nombre (q•0) qui soit ≥B(b(n)) donc, par définition de B(N), l'entier q (qui code le programme en question) est lui-même >b(n). Définissons maintenant le programme p_n suivant : il reçoit une entrée q, qu'il interprète comme un entier naturel, il exécute le programme codé par n pendant au plus q étapes (je n'ai pas échangé les noms !, c'est bien n qui est exécuté comme programme pendant un nombre d'étapes donné par la valeur de q), et, si l'exécution s'est terminée dans le temps imparti, il renvoie ⟨0,q•0⟩, sinon il renvoie ⟨1,0⟩. D'après ce qu'on vient de dire sur la valeur de q, le programme p_n est dans (☇☇D_n⇛D_n) ⇛ (D_n⊔☇D_n). Par conséquent, r appelé sur p_n doit renvoyer un élément de ☇☇D_n⊔☇D_n, donc selon qu'il est de la forme ⟨0,—⟩ ou ⟨1,—⟩ je sais que n termine ou pas et je renvoie oui ou non.

Bref, mon programme résout le problème de l'arrêt, ce qui n'était pas possible. D'où la contradiction : le programme r ne peut pas exister, et la formule de Scott n'est pas réalisable.

Que signifient toutes ces formules ?

Quelle est la signification profonde de toutes ces formules ? Je n'ai pas de réponse à ça, et comme je l'ai déjà dit, de ce que je sache, personne n'en a. Les mathématiciens soviétiques ont produit au compte-goutte des formules réalisables non démontrables, et quasiment toute question qu'on peut imaginer est ouverte.

(Si on veut un exemple explicite de question ouverte qui devrait sans doute être attaquable, la formule qui vient un cran plus haut en complexité que la formule de Scott, parfois appelée formule anti-Scott, à savoir (((¬¬D⇒D) ⇒ (D∨¬D)) ⇒ (¬¬D∨¬D)) ⇒ (¬¬D ∨ (¬¬D⇒D)) — c'est-à-dire (formule de Scott) ⇒ (¬¬D ∨ (¬¬D⇒D)), et elle n'est ni plus forte ni plus faible que la formule de Scott — : de ce que je comprends, on ignore si elle est réalisable. Autrement dit, est-ce qu'à partir d'un réalisateur de la formule de Scott pour D on peut réussir à produire soit une promesse que D est habité soit un élément potentiel de celui-ci ?)

Je peux reprendre l'agitage de main de mon introduction en disant que je pense que c'est important de regarder bien attentivement ces formules réalisables en espérant qu'elles nous apprennent quelque chose sur la calculabilité (ou sur les limitations du typage), parce qu'elles font partie de la logique naturelle de la calculabilité.

Je peux quand même dire un mot sur un point : l'importance des promesses : j'ai évoqué plus haut un résultat (de Medvedev et Plisko) selon lequel toute formule propositionnelle sans ‘⊥’ (donc sans ‘¬’) qui est réalisable est, en fait, démontrable. Ça veut dire que la divergence entre réalisabilité et démontrabilité (ou peut-être que je devrais dire, entre pouvoir du monde non typé et pouvoir du monde typé) concerne des formules avec des promesses, ces fameux objets sans contenu informatif mais dont la seule existence garantit une vérité logique. C'est pour ça que les formules considérées dans tous les exemples regorgent de symboles ‘¬’ : quand une variable A apparaît uniquement sous la forme ¬A, c'est que ce n'est pas vraiment une partie de ℕ, c'est un booléen caché (le booléen étant représenté par est-ce que la partie A est vide, et il est caché parce que l'algorithme qu'on construit n'a pas accès à sa valeur ; dans le contexte du topos effectif, l'objet des booléens cachés est l'objet ∇2 si on sait ce que c'est). Peut-être que ça ouvre la porte à de nouvelles réflexions.

Formules réalisables vs. autres degrés de calculabilité

Autre piste de réflexion possible : tout ce que j'ai raconté s'applique presque mot pour mot à toutes sortes d'autres formes de calculabilité. Dans quelle mesure changer la calculabilité considérée change-t-il ce qui est réalisable comme formule propositionnelle ?

À première vue, pas grand-chose : tout ce que j'ai raconté se transpose, il me semble, à d'autres degrés de Turing (au sens ordinaire), c'est-à-dire à des machines de Turing disposant de n'importe quel oracle ℕ→ℕ donné.

Néanmoins, comme je l'avais expliqué dans ce billet, la notion d'oracle se généralise à des fonctions plus générales (fonctions partielles, fonctions non-déterministes ou même « fonctions avec conseil »). Et là, pour ceux qui ont lu le billet en question, je peux faire quelques remarques. Pour ces oracles généralisés, les choses sont différentes, essentiellement par le fait que ces oracles permettent d'avoir accès aux parties pour lesquelles on essaye de réaliser la formule (Nimué les voit et peut éventuellement essayer de conseiller Arthur). Par exemple, il est assez évident qu'avec l'oracle « omniscient » noté ॐ ou Error_½ dans ce billet, on tombe sur la logique classique. Inversement, on doit pouvoir transformer une formule propositionnelle non-réalisable en oracle généralisé, l'oracle fournissant justement un réalisateur de la formule (Nimué choisit les parties, puis Merlin choisit un réalisateur). Il faudrait essayer de trouver une connexion avec cet article.

Ceci dit, monter dans la puissance de calculabilité n'est pas forcément la seule approche possible. Par exemple, il est bien connu en typage que la logique classique s'obtient par l'introduction de la fonction call/cc au langage, et il y a des extensions de la réalisabilité dans ce contexte (cf. ici par exemple). Maintenant, la logique propositionnelle classique est très pauvre, donc ce n'est pas très intéressant dans l'optique que j'ai évoquée dans ce billet. Mais peut-être qu'on peut trouver une sorte de version faible du call/cc qui réalise, disons, la formule de Kreisel-Putnam ou celle de Scott ? (Autrement dit, vu qu'on a des logiques intermédiaires entre logique intuitionniste et logique classique définies par les formules de Kreisel-Putnam et de Scott — séparément ou ensemble — on devrait aussi avoir des notions intermédiaires entre la réalisabilité et la réalisabilité classique.) À méditer.

Calculabilité sur ℕ^ℕ ?

Je ne veux pas entrer dans la définition un peu pénible d'une algèbre combinatoire partielle (cf. par exemple ici), mais disons juste un mot sur la seconde algèbre de Kleene.

Il y a une analogie entre les fonctions calculables partielles ℕ⇢ℕ et les fonctions continues ℕ^ℕ ⇢ ℕ^ℕ (où ℕ^ℕ est l'« espace de Baire » des suites d'entiers, muni de la topologie produit de la topologie discrète) dont le domaine de définition est un G_δ, c'est-à-dire une intersection dénombrable d'ouverts. Pour faire marcher cette analogie, on a besoin du fait que, de même qu'une fonction partielle calculable ℕ⇢ℕ peut être codée par un entier naturel e (un programme qui la calcule), ce qui donne naissance à la « première algèbre de Kleene » (ℕ muni de (e,n)↦e•n), on peut coder une fonction continue ℕ^ℕ ⇢ ℕ^ℕ dont le domaine de définition est un G_δ par un élément de ℕ^ℕ (pour les détails, voir ici ou là ou vers la fin de mon billet sur le topos effectif), ce qui donne naissance à la « seconde algèbre de Kleene », c'est-à-dire ℕ^ℕ muni de l'opération consistant (ε,α)↦ε•α consistant à appliquer à α∈ℕ^ℕ la fonction codée par ε∈ℕ^ℕ. (Le codage des couples ne pose aucune difficulté particulière : on peut par exemple entrelacer les valeurs des deux fonctions.)

Une fois qu'on a défini cette seconde algèbre de Kleene, on peut refaire toute la définition de la réalisabilité propositionnelle sur ℕ^ℕ au lieu de ℕ, simplement maintenant elle parle de continuité sur ℕ^ℕ au lieu de parler de calculabilité sur ℕ. Question naturelle : que peut-on dire des formules propositionnelles réalisables (par un élément de ℕ^ℕ) ? Et que peut-on dire de celles qui sont réalisables par un élément de ℕ^ℕ qui soit lui-même calculable (au sens usuel, de Church-Turing) en tant que fonction ℕ→ℕ ? Ces deux notions correspondent respectivement à la logique (propositionnelle) interne du « topos de la réalisabilité fonctionnelle » et du « topos de Kleene-Vesley », auxquels j'avais brièvement fait allusion dans mon billet sur le topos effectif, exactement comme la réalisabilité fonctionnelle sur ℕ (i.e., sur la première algèbre de Kleene) définie dans l'ensemble de ce billet est la logique (propositionnelle) interne du topos effectif.

Pour rendre ça moins abstrait, on s'intéresse à des manipulations non plus d'entiers naturels mais de flux d'entiers naturels (i.e., des suites, mais il vaut mieux y penser comme des flux, parce que le principe de la continuité/calculabilité dont il est question ici est justement qu'on prend des décisions sur la base de préfixes finis du flux), et on demande à réaliser des contrats, représentés par des formules propositionnelles, sur ces manipulations, soit juste continues, soit calculables (au sens des machines de Turing de type 2).

Je ne sais essentiellement rien sur la question. Les arguments que j'ai exposés plus haut pour la réalisabilité propositionnelle des formules de Ceitin, de Rose, de Plisko, etc., sont particuliers à la calculabilité de Church-Turing (i.e. « de type 1 ») : notamment, dans la seconde algèbre de Kleene, il ne semble pas qu'on puisse[#9] « lancer en parallèle » deux calculs, donc tous les arguments s'effondrent. Ça ne veut pas dire que la conclusion ne vaut pas : je n'ai ni réussi à prouver que ces formules sont réalisables ni qu'elles ne le sont pas (certes, je n'y ai pas passé des heures non plus). J'ai posé la question sur MathOverflow, mais sans réponse (mais aussi sans obtenir beaucoup d'attention, donc ça ne prouve pas grand-chose).

[#9] Voici en tout cas quelque chose de précis : la fonction ℕ^ℕ ⇢ ℕ^ℕ qui vaut 0 (i.e., la fonction nulle) partout sauf en 0 où elle n'est pas définie, est bien continue définie sur un G_δ ; celle qui vaut 1 (disons la fonction valant 1 en 0 et 0 ailleurs, mais prenez la fonction constamment 1 si vous préférez) en 0 et non définie ailleurs, est également (trivialement) continue et définie sur un G_δ. Mais si on essaie de les recoller, on obtient la fonction qui vaut 1 en 0 et 0 ailleurs, et celle-ci n'est pas définie. Ceci montre qu'on ne peut pas, dans la seconde algèbre de Kleene, prendre deux fonctions partielles « calculables » et trouver une fonction « calculables » définie sur la réunion de leurs ensembles de définition et qui vaut partout la valeur d'une des deux fonctions données (alors que dans la première algèbre de Kleene on peut, justement en lançant les calculs en parallèle et en renvoyant le résultat du premier qui termine).