La pause café de ce midi a été agitée par un débat sur une question qui revient fréquemment: est-il possible de rajouter le tiers exclus à ma théorie des types préférée sans tout casser ?

Point de départ

Les avis divergent évidemment sur ce que l'on met dans une théorie des types et quelles sont les propriétés essentielles à préserver. Je vais employer ici une théorie des types à la Martin-Löf:

• quelques types inductifs de base (type vide \(\bot\), booléens \(\mathbb{B}\), entiers naturels \(\mathbb{N}\)),
• des sommes \(\Sigma\) et produits dépendants \(\Pi\),
• une hiérarchie d'univers prédicatifs \(\square_i\) et
• un type identité \(x =_A y\).

On munit cette théorie d'une relation de conversion \(\vdash t \equiv u : A\) entre termes de même types $A$ induite par la \(\beta\)-réduction \((\lambda x: A.~t)~u \leadsto t[u/x]\) et les réductions des éliminateurs sur les inductifs (par exemple \(\texttt{ind}_{\mathbb{B}}~P~h_{\texttt{true}}~h_{\texttt{false}}~\texttt{true} \leadsto h_{\texttt{true}}\)).

Une telle théorie admet un algorithme de typage décidable reposant en particulier sur la décidabilité de la conversion ainsi que la propriété de canonicité que l'on énoncera ici de la manière suivante:

Tout terme clos de type booléen est convertible à une valeur canonique:

\[ \vdash t : \mathbb{B} \quad\implies\quad \vdash t \equiv \texttt{true} : \mathbb{B} \quad\vee \quad\vdash t \equiv \texttt{true} : \mathbb{B} \]

La question du jour

Le débat a été lancé par la question suivante:

Est-il possible de rajouter le tiers exclus sur les h-propositions tout en conservant la décidabilité du typage et la canonicité ?

Les h-propositions dans la question sont des types qui ont prouvablement au plus un habitant, c'est à dire

Le jargon vient de HoTT, et le HoTTBook étudie en détail les propriétés de cette classe de type, notamment, \(\bot\) est une h-proposition.

On pourrait s'attendre à ce que \(p \to q\) soit une h-proposition dès que \(p\) et \(q\) le sont, mais sans supposition supplémentaire sur notre théorie, on ne peut pas dire grand chose sur l'égalité entre fonctions \(f,g : p \to q\)...

Pour aller plus loin on suppose l'extensionalité des fonctions, que deux fonctions sont égales dès qu'elles sont égales point à point:

Sous cette hypothèse, \(\forall x: A, p x\) est une h-proposition dès que \(p : A \to \texttt{hProp}\). En particulier, \(\neg A := A \to \bot\) est une hProposition pour tout type \(A\) et pour toute h-proposition \(p\), \(p+\neg p\) est encore une h-proposition.

Et le tiers-exclus à valeur dans les h-propositions s'énonce alors comme \(\texttt{em} : \forall (p : \texttt{hProp}). p + \neg p\).

C'est grave docteur ?

L'avis des éminences éclairées participant à ce débat était que ça semblait difficile d'avoir le beurre (le tiers-exclus) et l'argent du beurre (la canonicité et la décidabilité de la conversion).

Le problème fondamental est que même à valeur dans les h-propositions, on peut extraire de l'information du résultat de notre tiers exclus en faisant une analyse de cas sur le \(+\). Si \(\vdash p : \texttt{hProp}\) est une h-proposition close, le booléen clos \(\vdash b_p := \texttt{ind}_{+}~(\lambda x. \mathbb{B})~\texttt{true}~\texttt{false}~(\texttt{em}~p) : \mathbb{B}\) représente le fait que la h-proposition \(p\) est habitée. On peut ensuite appliquer la canonicité pour obtenir \(\vdash b_p \equiv \texttt{true} : \mathbb{B}~ \vee \vdash b_p \equiv \texttt{false} : \mathbb{B}\), et comme on a supposé notre conversion décidable, on peut tester lequel des deux cas est réalisé.

Sans être surprenante la réduction à de quoi laisser dubitatif: que se passet-il si on applique à une h-propositions pas très gentille, par exemple au problème de l'arrêt ? Est-ce que l'on ne vient pas de décider une proposition indécidable ?

Nos digressions ne nous ont pas permis d'obtenir un contre-exemple aussi direct, mais après quelques contorsions nous avons obtenu un résultat qui semble enterrer certains espoirs naïfs que je me faisais sur la Théorie des Types.

Un mélange explosif

Supposons donc que l'on puisse construire une variante de MLTT telle que décrite plus haut vérifiant canonicité et conversion décidable avec le tiers-exclus \(\texttt{em}\) pour les h-propositions. On montre que l'on peut dériver une contradiction.

Première étape, on dérive le principe de Markov et l'indépendance des prémisses.

Le principe de Markov \(\texttt{MP}(P)\) stipule que pour un prédicat décidable sur les entiers \(\vdash P : \mathbb{N}\to \mathbb{B}\), on peut extraire des témoins validant le prédicat juste en "sachant" qu'ils existent:

où l'on abrège \(\exist_{\texttt{min}}n.~P~n := \Sigma(n : \mathbb{N}).~P~n \wedge (\forall m.~P~m \to m \geq n)\). Pour le dériver depuis le tiers-exclus, on utilise la tautologie \((\neg\neg Q \to Q) \iff (Q \vee \neg Q)\) avec \(Q := \exist_{\texttt{min}}n.~P~n\) en observant que \(Q\) est une h-proposition.

L'indépendance des prémisses \(\texttt{IP}(h,P)\) établit que si l'on peut trouver un entier satisfaisant le prédicat décidable \(P\) sous l'hypothèse de \(\neg h\) (où h est une h-proposition niée, donc "purement logique"), alors on aurait pu produire cet entier sans avoir accès à \(\neg h\):

On prouve l'indépendance des prémisses en appliquant le tiers-exclus à \(h\):

• Si \(h\) tient, alors on retourne n'importe quel entier, par exemple \(0\) et la "preuve" que \(\neg h \to P~0\) consiste simplement à utiliser la contradiction entre \(h\) et \(\neg h\);
• Sinon on a une preuve de \(\neg h\) et on peut l'appliquer à l'hypothèse de \(\texttt{IP}\).

Deuxième étape, on applique \(\texttt{IP}\) à \(\texttt{MP}\):

Donc à partir de n'importe quel prédicat décidable \(P : \mathbb{N} \to \mathbb{B}\), on fabrique un entier \(n_P\) tel que si \(\neg\neg (\exists_{\texttt{min}}n.~P~n)\) alors \(P~n_P\). En particulier, une machine de Turing \(\texttt{M}\) induit un prédicat \(P_\texttt{M}\) qui est vrai si \(\texttt{M}\) termine en \(n\) étapes, et \(P_{\texttt{M}}~n_{P_{\texttt{M}}}\) décide l'arrêt de \(\texttt{M}\). En effet, supposons par l'absurde que ce ne soit pas le cas, c'est à dire que \(P_{\texttt{M}}~n_{P_{\texttt{M}}} \equiv \texttt{false}\) mais que \(\texttt{M}\) termine. Comme \(\texttt{M}\) termine, on peut construire une preuve de \(\neg\neg (\exists_{\texttt{min}}n.~P~n)\), par exemple en exécutant la machine \(\texttt{M}\) et en calculant effectivement le nombre d'étapes qu'il lui faut pour terminer, que l'on utilise pour conclure que \(P_{\texttt{M}}~n_{P_{\texttt{M}}} \equiv \texttt{true}\), contredisant notre hypothèse.

Bref, on est capable d'une part de calculer pour chaque machine de Turing un booléen, de manière effective grâce à nos hypothèses, d'autre part de montrer que ce booléen est vrai si et seulement si la machine s'arrête. À ce que je sache, on vient donc de décider le problème (indécidable) de l'arrêt, contradiction.

Conclusion

Il semble donc difficile de rajouter le tiers-exclus dans les h-propositions tout en gardant des propriétés raisonnable sur le système. Plusieurs points m'embêtent tout de même dans ce raisonnement. Tout d'abord les invités "surprises" que sont l'extensionalité des fonctions et une apparition du tiers-exclus dans la métathéorie (pour le raisonnement par l'absurde du dernier paragraphe). Mais surtout l'aspect très alambiqué de cette preuve...