Je veux ici de nouveau parler d'informatique théorique, dans son intersection avec les maths (logique, calculabilité, typage), et plus précisément d'un sujet appelé la réalisabilité propositionnelle. Je reconnais qu'il a un petit côté « opération de pub » de ma part : il s'agit d'un sujet qu'on peut qualifier d'obscur, voire ésotérique (largement confiné à une poignée de publications soviétiques des années 1960–1990, dont certaines n'ont même pas été traduites du russe en quoi que ce soit d'autre[#], ce qui le dessert cruellement), et pourtant il me semble que d'une part il a des choses à nous apprendre sur l'informatique, sur ce que peut ou ne peut pas faire un algorithme, et sur le rapport entre ça et le typage, et d'autre part il n'est techniquement pas très compliqué à exposer (j'en ai dit un mot — bien moins que ce qui va suivre, certes — dans mon cours à Télécom qui s'est récemment fini, et je ne crois pas avoir largué tout le monde). Donc je trouve qu'il mérite plus d'attention.
[#] Bon, le fait que ce soit en russe ne devrait pas être un obstacle sérieux, surtout maintenant qu'on a des OCR et des traducteurs automatiques, il n'y a vraiment plus de raison. Le problème, c'est que souvent, et en plus d'être en russe, l'article a le défaut d'être super mal écrit : extrêmement concis et pas toujours super rigoureux comme les mathématiciens soviétiques avaient tendance à l'être, références vagues, et fautes de frappe à foison. (Voyez par exemple cette question que j'ai posée sur MathOverflow en essayant de comprendre l'argument de Ânkov sur la non-réalisabilité de l'axiome de Scott que j'expose plus bas ici de façon, j'espère, nettement plus clair que le texte original : mon russe est enfoui au fond des oubliettes, mais ce n'est vraiment ce qui était le plus problématique en l'occurrence par rapport aux fautes de frappe et au style de rédaction vraiment minimaliste.)
Je ne sais pas si l'entrée de blog qui va suivre peut aider à convaincre qui que ce soit de s'y réintéresser, mais en tout cas, si on lit ce qui suit on pourra se dire qu'on sait une proportion significative de tout le savoir de l'Humanité sur la réalisabilité propositionnelle (i.e., pas grand-chose !), et il n'y a pas beaucoup de sujets techniques pour lesquels on puisse en dire autant.
Ajout () : Pour les gens qui veulent savoir de quoi ce billet cause mais qui n'ont pas la patience de lire ce pavé (ni même l'introduction), j'ai écrit un résumé en seulement 13 tweets, ici sur Twitter et ici sur BlueSky [on peut lire le fil BlueSky sans avoir de compte dessus].
Table des matières
Résumé et publicité préalable
Avant de rentrer dans le cœur du sujet,
j'essaie d'expliquer
informellement[#2] (et de
manière — j'espère — assez peu technique) de quoi il s'agit, et
pourquoi je pense que c'est assez intéressant pour prendre le temps de
déchiffrer des articles à moitié oubliés dans des journaux soviétiques
et de pondre un pavé de 1729 pages dans ce blog pour réexpliquer le
tout aux enfants. (Si on veut
passer directement à la
définition, c'est possible, mais je pense que c'est intéressant de
donner d'abord une idée grossière de ce dont je vais parler, au risque
de prendre un peu un ton introduction de manuscrit de thèse
.
Je remercie d'ailleurs mes peluches pour leur soutien et leur patience
tout au long de l'écriture de cette entrée.)
[#2] Autrement dit,
comme le corps de cette entrée est très long, je commence par une
introduction très longue pour essayer de motiver cette
longueur. Je n'ai fait celle-ci plus longue que parce que je n'ai
pas eu le loisir de la faire plus courte.
(Blaise Pascal)
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.
Définition de la réalisabilité propositionnelle, exemples et remarques
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 deP⇛∅
(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 depromesse
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.
Extension aux quantificateurs propositionnels
Je passe en petits caractères pour mentionner une petite extension naturelle à ce point, même si je ne m'en servirai pas ensuite (on peut donc sauter cette section).
On appelle formule propositionnelle du second ordre une formule obtenue avec les constructions des formules propositionnelles simples que j'ai déjà expliquées, plus deux nouvelles constructions permettant de quantifier sur les variables propositionnelles : si φ(A) est une formule propositionnelle du second ordre ayant peut-être la variable propositionnelle libre A, alors ∀A.φ(A) et ∃A.φ(A) sont deux nouvelles formules propositionnelles du second ordre dans lesquelles la variable A est liée par le quantificateur (donc elle n'est plus libre, et les conventions habituelles sur le renommage des variables liées ont cours). La réalisabilité de telles formules est définie en étendant les règles précédemment données par :
- ⟦∀A.φ(A)⟧ = ⋂P⊆ℕ ⟦φ⟧(P)
- ⟦∃A.φ(A)⟧ = ⋃P⊆ℕ ⟦φ⟧(P)
Avec cette définition, et surtout avec la bonne notion de démonstration, l'analogue naturel des résultats évoqués ci-dessus vaut encore. La notion de démonstration, et le Curry-Howard qui va bien, sont ici ceux du système F de Girard, et je l'ai évoqué un peu dans ce bout de mon billet sur Curry-Howard.
L'introduction de ces quantificateurs explicites a le mérite d'éclaircir les choses sur l'uniformité : quand on dit qu'une formule propositionnelle simple φ(A,B,C,…) est réalisable, on veut en fait dire que la formule propositionnelle du second ordre close ∀A. ∀B. ∀C. ⋯ φ(A,B,C,…) obtenue en quantifiant universellement toutes les variables propositionnelles libres, est réalisable.
Un mot sur le rapport avec la réalisabilité de Kleene
Cette question est aussi en petits caractères, et comme elle est assez technique on est invité à la sauter si on n'a pas lu le billet sur la réalisabilité de Kleene, mais je me dis qu'il faut quand même que je dise un mot sur le rapport, qui est malheureusement un peu embrouillé.
La notion la plus standard, et aussi la plus ancienne, de
réalisabilité (dite de Kleene
) travaille sur des formules
de l'arithmétique du premier ordre (c'est-à-dire formées au moyen
des connecteurs logiques ‘∧’, ‘∨’, ‘⇒’, ‘⊤’, ‘⊥’ mais aussi des
quantificateurs ‘∀’, ‘∃’ portant sur les entiers naturels — et non pas
les variables propositionnelles comme à la section précédente — à
partir des formules arithmétiques atomiques qui sont des égalités
entre deux termes arithmétiques ; et il n'y a pas du tout de variables
propositionnelles dans l'histoire). La définition de la réalisabilité
pour ces formules-là est donnée
dans mon billet à ce sujet (on peut
se contenter de la définir pour les formules closes,
c'est-à-dire sans variable libre, et c'est ce que je fais dans le
billet en question).
On peut donc légitimement se demander quel est le rapport entre la réalisabilité de Kleene (pour l'arithmétique du premier ordre, donc) et la réalisabilité propositionnelle que j'ai définie et que je vais temporairement qualifier de « native ». En fait, c'est un peu le bordel ! A priori je peux définir au moins quatre notions différentes (voire cinq si je compte la version non-uniforme évoquée plus haut, mais on a vu qu'elle n'avait pas d'intérêt) de la réalisabilité pour une formule propositionnelle φ(A,B,C,…) :
- On peut dire qu'elle est nativement uniformément réalisable pour désigner la notion que j'ai définie ci-dessus dans le présent billet, c'est-à-dire lorsque ⋂P,Q,R,… ⊆ ℕ ⟦φ⟧(P,Q,R,…) est habitée (i.e., il y a un même entier r qui appartienne à ⟦φ⟧(P,Q,R,…) quelles que soient les parties P,Q,R,… quelconques de ℕ).
- On peut dire qu'elle est uniformément réalisable au sens de Kleene lorsqu'il existe un même entier r qui, quelles que soient les formules arithmétiques closes du premier ordre χa,χb,χc,…, réalise au sens de Kleene la formule φ(χa,χb,χc,…) obtenue en les substituant aux variables propositionnelles A,B,C,… de φ.
- On peut dire qu'elle est effectivement réalisable au sens de Kleene lorsqu'il existe un algorithme qui, données des formules arithmétiques closes du premier ordre χa,χb,χc,…, réalise au sens de Kleene, produit un entier qui réalise la formule φ(χa,χb,χc,…) obtenue en les substituant aux variables propositionnelles A,B,C,… de φ.
- On peut dire qu'elle est réalisable au sens de Kleene lorsque, quelles que soient les formules arithmétiques du premier ordre χa(n,…),χb(n,…),χc(n,…),… admettant possiblement des variables libres n,…, la formule ∀n. ∀⋯ φ(χa(n,…),χb(n,…),χc(n,…),…) obtenue en les substituant aux variables propositionnelles A,B,C,… de φ et en quantifiant universellement sur les variables libres n,…, est réalisable au sens de Kleene.
(La terminologie est franchement pourrie. Dans le survey de Plisko
référencé dans l'introduction, la notion (1), celle qui m'intéresse le
plus ici, n'est évoquée que dans le cas plus général de l'arithmétique
du second ordre et est appelée absolutely
realizable
, mais dans le contexte un peu différent de la logique
du second ordre ; et les autres sont appelées respectivement
(2) uniformly realizable
,
(3) effectively realizable
et
(4) irrefutable
. J'ai essayé d'ajouter des
précisions pour rendre ces termes moins pourris.)
Je m'intéresse dans ce billet à la notion (1) à la fois parce qu'elle me semble la plus simple et la lus naturelle, et aussi parce que c'est la logique interne du topos effectif. Les mathématiciens soviétiques des années des années 1960–1990 se sont, je crois, concentrés sur les notions (2)–(4), et en fait surtout (4).
Il n'est pas difficile de voir que ces notions sont rangées
ci-dessus dans l'ordre de la plus forte à la plus faible : chacune
implique la suivante. Néanmoins, pour autant que je
sache, on ignore si ces implications sont réversibles (Plisko
le dit explicitement pour (2)⇒(3) et (3)⇒(4), et concernant (1)⇒(2) je
ne trouve juste pas de discussion à ce sujet). Le fait est que chaque
exemple connu d'une formule propositionnelle réalisable est réalisable
dans le sens le plus fort de tous, celui que j'ai appelé
(1) nativement uniformément réalisable
et qui est l'objet de ce
billet, et inversement, chaque exemple connu d'une formule
propositionnelle irréalisable ne l'est pas même dans le sens le plus
faible, (4) (i.e., elle est irréalisable au sens de Kleene).
Bref, on a quatre notions a priori différentes, ci-dessus listées de la plus forte à la plus faible, mais pour autant qu'on sache il est plausible qu'elles coïncident. C'est un peu embarrassant. Mais comme je l'ai dit, pour chaque formule intéressante qu'on connaisse, soit on prouve la notion la plus forte, soit on réfute la plus faible.
Comme les résultats positifs (telle formule φ est réalisable) m'intéressent plus que les négatifs, il est naturel que je me focalise sur la notion la plus forte de réalisabilité. Mais il faudrait ajouter, concernant les résultats négatifs, une explication de comment ils réfutent même la notion la plus faible ; sur les deux cas « intéressants » que je vais évoquer plus bas, ce n'est pas plus difficile que je cas que je traite, donc je n'entre pas dans les détails.
À titre d'exemple simple, j'ai expliqué plus haut
que A ∨ ¬A n'est pas réalisable au sens (1),
i.e., pas nativement uniformément réalisable : l'idée-clé était qu'un
programme réalisant cette formule serait censé, sans avoir accès à une
partie P⊆ℕ, arriver à produire soit un élément
de P soit une promesse qu'elle est vide, et ce n'est
évidemment pas possible vu qu'il n'a pas accès à la partie.
Maintenant envisageons la réalisabilité de cette même formule pour le
sens le plus faible (4), et montrons qu'elle n'est même pas
(4) réalisable au sens de Kleene. Cette fois il faut trouver une
formule χ(n) du premier ordre telle que
∀n. χ(n) ∨ ¬χ(n)
ne soit pas réalisable au sens de Kleene. Or un
tel χ(n) est fourni par une formule du
style la n-ième machine de Turing termine
: un
réalisateur de
∀n. χ(n) ∨ ¬χ(n)
devrait décider le problème de l'arrêt. Autrement dit, cette fois
l'argument est un peu plus raffiné : le programme a accès
à n, mais il n'arrive quand même pas à produire soit un
réalisateur de χ(n) soit une promesse
que χ(n) est irréalisable.
Réalisabilité de diverses formules
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.
La preuve de ⓐ n'est pas ce qui m'intéresse le plus ici, donc je la mets en petits caractères et on peut l'ignorer, mais je vais quand même en donner une pour la complétude de ce billet et pour donner une idée de comment on peut faire ce genre de choses. Elle est basée sur le fait qu'on peut interpréter le calcul propositionnel intuitionniste par les ouverts d'un espace topologique X quelconque, et en l'occurrence je prendrai ℝ² : je rappelle de quoi il s'agit et comment ça fonctionne dans le paragraphe qui suit.
La sémantique des
ouverts (une sorte de digression) : Soit X un
espace topologique, ou simplement ℝn.
Pour U et V sont deux ouverts de X on
notera disons disons U⇴V
(« opération de
Heyting ») l'intérieur de V∪(X∖U),
c'est-à-dire le plus grand ouvert W tel
que U∩W ⊆ V∩W (ou encore,
l'ensemble des points au voisinage desquels on
a U⊆V). Pour toute formule
propositionnelle φ(A,B,C,…)
et tous ouverts U,V,W,…
de X on définit un ouvert noté disons
⌞φ⌟(U,V,W,…)
de X en remplaçant ‘∧’, ‘∨’, ‘⇒’, ‘⊤’ et ‘⊥’ par
respectivement ‘∩’ (intersection), ‘∪’ (union), ‘⇴’ (l'opération de
Heyting que je viens de définir), ‘X’ et ‘∅’ et bien sûr
chaque variable A,B,C,… par
l'ouvert U,V,W,… qu'on a choisi de
mettre à la place. (Noter que ¬A
se transforme
en U⇴∅, qu'on pourrait noter ~U, c'est-à-dire
l'intérieur du complémentaire de U ou encore le plus grand
ouvert disjoint de U.) Cette sémantique des ouverts
est correcte et complète
(Tarski, 1938), c'est-à-dire
que φ(A,B,C,…) est
intuitionnistement démontrable si et seulement si pour tout
espace topologique X (ou même seulement
pour X=ℝn pour un n≥1 fixé
quelconque) et pour tous
ouverts U,V,W,… on a
⌞φ⌟(U,V,W,…)
= X (l'espace tout entier).
Pour prouver que (¬(A₁∧A₂) ∧ (¬A₁⇒(B₁∨B₂)) ∧ (¬A₂⇒(B₁∨B₂))) ⇒ ((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨ (¬A₂⇒B₁) ∨ (¬A₂⇒B₂)) n'est pas démontrable, il suffit donc que je trouve un espace topologique X (ce sera ℝ²) et quatre ouverts U₁,U₂,V₁,V₂, tels que l'ouvert (~(U₁∩U₂) ∩ (~U₁⇴(V₁∪V₂)) ∩ (~U₂⇴(V₁∪V₂))) ⇴ ((~U₁⇴V₁) ∪ (~U₁⇴V₂) ∪ (~U₂⇴V₁) ∪ (~U₂⇴V₂)) (appelons-le W) ne soit pas égal à X tout entier.
Voici une possibilité (dans ℝ², donc) : prenons pour U₁ le demi-plan {(x,y) : x<0}, pour U₂ le demi-plan {(x,y) : x>0}, pour V₁ l'ouvert {(x,y) : y > −x²} et pour V₂ l'ouvert {(x,y) : y < x²} (pour un dessin, voir cette feuille d'exercices, dans le corrigé ce qui est actuellement l'exercice 4.5 ; noter que ~U₁ = U₂ et que ~U₂ = U₁). Alors (~(U₁∩U₂), (~U₁⇴(V₁∪V₂)) et (~U₂⇴(V₁∪V₂))) sont tous les trois le plan ℝ² tout entier. En revanche, aucun des ouverts (~U₁⇴V₁), (~U₁⇴V₂), (~U₂⇴V₁) ni (~U₂⇴V₂) ne contient l'origine (0,0). Donc l'origine n'est pas dans l'ouvert W défini par la formule de Ceitin, et celle-ci n'est pas démontrable.
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 Pi est vide et renvoyant un élément de Qj, 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 ei 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 ei 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 ☇Pi⇛Qj.
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,qs⟩⟩ si c'est e₁ qui a fourni la valeur ou ⟨1,⟨k,qs⟩⟩ si c'est e₂ qui l'a fournie, où qs est un programme qui ignore la valeur t passée en argument et renvoie toujours s.
En fait, si on y reréfléchit, ce r réalise une formule un tout petit peu plus générale (proposée par Skvorcov) :
(¬(A₁∧A₂) ∧
(¬A₁⇒(B₁∨B₂)) ∧
(¬A₂⇒(C₁∨C₂)))
⇒
((¬A₁⇒B₁) ∨ (¬A₁⇒B₂) ∨
(¬A₂⇒C₁) ∨ (¬A₂⇒C₂))
En revanche, la formule (¬A⇒(B₁∨B₂)) ⇒ ((¬A⇒B₁) ∨ (¬A⇒B₂)) (« formule de Kreisel-Putnam »), elle, n'est pas réalisable, et je vais y revenir plus bas.
*
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 qA renvoie
toujours A (i.e., promet que s'il y a un snark il y en a un
en A) et l'autre qB
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 qA
et qB 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 qA remplit bien la contrainte
demandée, donc la copie de p qui a
reçu qA 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 qA 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 qA en entrée (mais il y a
forcément un snark, parce que s'il n'y en avait
pas, qA 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 qA et qB : 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 qA et qB, 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 pA et pB, 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 pA et pB sur un programme qn qui juste renvoie n, jusqu'à trouver un n pour lequel l'un des deux programmes p appelé sur qn 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 qn 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 qn le programme qui juste renvoie n et on lance en parallèle p sur ⟨0,qn⟩ et sur ⟨1,qn⟩, autrement dit, en prétendant que qn envoie A dans C₁ et en prétendant que qn envoie A dans C₂, et ce, jusqu'à tomber sur un n et un i∈{0,1} pour lesquels p termine sur ⟨i,qn⟩ 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 qn (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,qn⟩ 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.
Non-réalisabilité de diverses formules
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,qt⟩
où qt 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,qn⟩
où qn est la fonction constante de
valeur n, et s'il le trouve dans W₂, il termine
et renvoie ⟨1,qn⟩
où qn 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, à savoir la réaliser en faisant appel à l'oracle de l'arrêt.
[Le paragraphe suivant a été modifié le : j'avais initalement fait avec deux sauts de Turing, mais comme signalé par jeanas dans le commentaire daté , un seul saut de Turing suffit. Je refais l'argument en conséquence.]
Comment ? Supposons qu'on me fournisse un programme p
qui soit dans (☇☇D⇛D) ⇛
(☇☇D⊔☇D) (ou (☇☇D⇛D) ⇛
(D⊔☇D), peu importe). Imaginons que
j'appelle p sur le
programme qn qui renvoie
constamment n : distinguons trois cas pour voir ce qui se
passe. Cas ⓐ : D est vide (et n est
quelconque). Dans ce cas, qn
appartient forcément à ☇☇D⇛D (car ☇☇D
est vide), donc p appelé sur
ce qn va répondre correctement
(répondre correctement
, c'est-à-dire déclarer D
vide, i.e., répondre ☇D). J'insiste sur le fait
(pour D vide) ceci se produit
pour tout n. Cas ⓑ : n appartient
à D (qui est donc habité). Dans ce
cas, qn appartient encore à
☇☇D⇛D (car n∈D),
donc p appelé sur ce qn va
de nouveau répondre correctement (répondre correctement
,
c'est-à-dire cette fois déclarer D habité, i.e., répondre
☇☇D). Cas ⓒ : D est habité mais n
n'est pas dedans. Dans ce cas, n'importe quoi peut se produire quand
on appelle p sur qn : il
peut ne pas terminer, ou il peut renvoyer n'importe quoi. (Fin de la
discussion des trois cas.) D'après ce qu'on vient de voir, s'il
existe n tel que p appelé
sur qn déclare D habité,
on est sûr que D est habité (car dans le cas ⓐ, on
a vu qu'il déclarait toujours D vide) ; et réciproquement,
si D est habité, il existe bien un n tel
que p appelé sur qn
déclare D habité (on a vu dans le cas ⓑ que n'importe
quel n dans D convient). Bref, si je lance en
parallèle l'exécution de p sur tous
les qn en attendant de voir si l'un
d'eux déclare D habité (i.e., répond ☇☇D), ceci
va terminer si et seulement si D est habité.
Savoir si c'est le cas n'est pas possible sans magie, mais si je
dispose d'un accès à l'oracle de l'arrêt pour les machines de Turing,
alors je peux décider si l'exécution de p sur tous
les qn finira par répondre
☇☇D quelque part : si c'est le cas je peux
déclarer D habité, sinon le déclarer vide. Ça marche au
sens où ça remplit le contrat de la formule de Scott, mais, de
nouveau, j'ai eu besoin d'un saut de Turing.
Maintenant, expliquons pourquoi la formule de Scott n'est pas réalisable (sans la triche du paragraphe précédent consistant à invoquer un oracle, 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 Dn l'ensemble des entiers
naturels ≥h(n). En revanche, si le programme
codé par n ne termine pas en temps fini, on
pose Dn = ∅. Maintenant,
si q appartient à
☇☇Dn⇛Dn
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 pn 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 pn est
dans
(☇☇Dn⇛Dn)
⇛
(Dn⊔☇Dn).
Par conséquent, r appelé
sur pn doit renvoyer un élément de
☇☇Dn⊔☇Dn,
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.
Diverses pistes de réflexion ultérieure
Comme d'habitude, quand j'en arrive à ce point de la rédaction d'un billet, je suis trop fatigué pour conclure proprement, donc je balance un peu en vrac des idées de réflexion, pas forcément expliquées de façon très claire, et qui sont plus un bloc-note pour moi (TOTHINK!) qu'une tentative d'expliquer quoi que ce soit. Mais comme ce n'est peut-être pas complètement sans intérêt non plus, autant le publier.
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).