More on propositional realizability.

1 files changed, 249 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3dc9c75..db51856 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1936,6 +1936,7 @@ juste qu'il « existe » classiquement.
 \end{frame}
 %
 \begin{frame}
+\label{bhk-interpretation}
 \frametitle{L'interprétation de Brouwer-Heyting-Kolmogorov}
 
 Interprétation \alert{informelle/intuitive} des connecteurs de la
@@ -2075,6 +2076,7 @@ se réduit en $t_i$ (pour $i\in\{1,2\}$).
 \end{frame}
 %
 \begin{frame}
+\label{curry-howard-example-with-conjunction}
 \frametitle{Correspondance de Curry-Howard : exemple avec conjonction}
 
 \itempoint Transformons en programme la démonstration qu'on a donnée
@@ -4314,7 +4316,7 @@ de $X$ fournissent un modèle du calcul propositionnel intuitionniste :
 \textbf{Théorème} (Tarski) : la sémantique des ouverts est correcte et
 complète pour le calcul propositionnel intuitionniste :
 \begin{itemize}
-\item\underline{correction :} si $\varphi(A_1,\ldots,A_r)$ est une
+\item\underline{correction :} si $\varphi(A_1,\ldots,A_r)$ est un
   théorème du calcul propositionnel intuitionniste, alors quel que
   soit $X$ et $U_1,\ldots,U_r$ ouverts de $X$, on a
   $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ (l'espace tout entier) ;
@@ -4379,6 +4381,252 @@ Kreisel-Putnam ») n'est pas prouvable en logique intuitionniste (et
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Sémantique 3 : la réalisabilité propositionnelle}
+
+On reprend les notations de la calculabilité, mais on notera $\Phi_e
+\colon \mathbb{N} \dasharrow \mathbb{N}$ pour la $e$-ième fonction
+générale récursive (pour éviter un conflit de notation).
+
+\medskip
+
+On définit les opérations suivantes sur l'ensemble
+$\mathcal{P}(\mathbb{N})$ des parties de $\mathbb{N}$ :
+\begin{itemize}
+\item $P \dottedland Q = \{\langle m,n\rangle : m\in P, n\in Q\}$
+  (codage de Gödel du produit $P\times Q$)
+\item $P \dottedlor Q = \{\langle 0,m\rangle : m\in P\} \cup \{\langle
+  1,n\rangle : m\in Q\}$ (sorte de réunion disjointe)
+\item $(P \dottedlimp Q) = \{e \in \mathbb{N} : \Phi_e(P){\downarrow}
+  \subseteq Q\}$, ce qui signifie $\forall m\in P.\,
+  \Phi_e(m){\downarrow}\in Q$ (programmes définis sur tout $P$ et
+  l'envoyant dans $Q$)
+\item $\dottedtop = \mathbb{N}$\quad\itempoint $\dottedbot = \varnothing$
+\item notamment, $\dottedneg P$ vaut $\mathbb{N}$ si $P = \varnothing$
+  et $\varnothing$ sinon (« promesses » que $P=\varnothing$) ;
+\item notamment, $\dottedneg \dottedneg P$ vaut $\varnothing$ si $P =
+  \varnothing$ et $\mathbb{N}$ sinon (« promesses » que
+  $P\neq\varnothing$).
+\end{itemize}
+
+\medskip
+
+\itempoint Si $\varphi(A_1,\ldots,A_r)$ est une formule
+propositionnelle et $P_1,\ldots,P_r \in \mathbb{N}$, on définit
+$\dot\varphi(P_1,\ldots,P_r)$ de façon évidente (par induction).
+
+\smallskip
+
+\itempoint Si $n \in \dot\varphi(P_1,\ldots,P_r)$, on dit aussi que
+$n$ \textbf{réalise} $\varphi(P_1,\ldots,P_r)$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La réalisabilité propositionnelle}
+
+\itempoint Les définitions de $\dottedlimp,\dottedland,\dottedlor$
+suivent précisément l'idée informelle de l'interprétation de
+Brouwer-Heyting-Kolmogorov (transp. \ref{bhk-interpretation}) en les
+rendant précises avec des parties de $\mathbb{N}$ et des fonctions
+générales récursives.
+
+\medskip
+
+\itempoint On dit qu'une formule propositionnelle
+$\varphi(A_1,\ldots,A_r)$ est \textbf{réalisable} (plus précisément,
+« uniformément réalisable ») lorsqu'il existe un \alert{même entier}
+$n$ qui réalise $\varphi(P_1,\ldots,P_r)$ quels que soient
+$P_1,\ldots,P_r \subseteq \mathbb{N}$ :
+\[
+n \in \bigcap_{P_1,\ldots,P_r} \dot\varphi(P_1,\ldots,P_r)
+\]
+
+\medskip
+
+\itempoint\textbf{Théorème} (Dragalin, Troelstra, Nelson) : la
+sémantique de la réalisabilité est correcte pour le calcul
+propositionnel intuitionniste : si $\varphi(A_1,\ldots,A_r)$ est un
+théorème du calcul propositionnel intuitionniste, alors il existe $n$
+qui réalise $\varphi(P_1,\ldots,P_r)$ quels que soient $P_1,\ldots,P_r
+\subseteq \mathbb{N}$.
+
+\medskip
+
+{\footnotesize Mieux : ce $n$ se construit à partir de la preuve de
+  $\varphi$ : c'est une forme d'\alert{extraction d'algorithme}.}
+
+\smallskip
+
+\textcolor{brown}{En fait on peut voir ça comme une conséquence de
+  Curry-Howard.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La réalisabilité propositionnelle : exemple}
+
+\itempoint Essayons de réaliser $A\land B \Rightarrow B\land A$ : on
+cherche donc un même entier dans $P\dottedland Q \dottedlimp
+Q\dottedland P$ pour \emph{tous} $P,Q\subseteq\mathbb{N}$.
+
+\medskip
+
+\itempoint Autrement dit, on veut trouver un programme $e$ tel que
+$\Phi_e$ soit défini sur $P\dottedland Q = \{\langle m,n\rangle : m\in
+P, n\in Q\}$ et l'envoie dans $Q\dottedland P = \{\langle n,m\rangle :
+n\in Q, m\in P\}$ (sans connaître $P,Q$).
+
+\smallskip
+
+Il suffit de permuter les coordonnées du couple !
+
+\smallskip
+
+Mais c'est ce que faisait le programme $\lambda z.\langle \pi_2 z,
+\pi_1 z\rangle$ associé à la preuve via Curry-Howard
+(cf. transp. \ref{curry-howard-example-with-conjunction}) !
+
+\medskip
+
+\itempoint Ceci marche en général : pour réaliser $\varphi$ où
+$\varphi$ est prouvable, on prend le $\lambda$-terme de preuve, on
+oublie les types (tout est entier !), on interprète l'application
+d'une fonction $f$ sur $n$ comme $\Phi_f(n)$, les couples et les
+sommes comme dans $\dottedland$ et $\dottedlor$, et le programme en
+question réalise $\varphi$ quels que soient $P_1,\ldots,P_r$
+puisqu'ils correspondent à des types dans le terme de preuve.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La réalisabilité propositionnelle : contre-exemples}
+
+\itempoint La formule $A\lor\neg A$ n'est pas réalisable : il
+s'agirait de trouver un \alert{même} entier qui \alert{quel que soit
+  $P$} soit de la forme $\langle 0,n\rangle$ avec $n\in P$ ou bien de
+la forme $\langle 1,n\rangle$ si $P=\varnothing$.  Visiblement c'est
+impossible (sans information sur $P$) !
+
+\medskip
+
+\itempoint La formule $\neg\neg A \Rightarrow A$ n'est pas
+réalisable : il s'agirait de trouver un \alert{même} programme qui, si
+$P$ est non-vide (si bien que $\dottedneg\dottedneg P = \mathbb{N}$),
+termine sur n'importe quel entier et renvoie un élément de $P$.
+Visiblement c'est impossible (sans information sur $P$) !
+
+\medskip
+
+\itempoint Plus subtilement, $(\neg\neg A \Rightarrow A) \Rightarrow
+(A\lor\neg A)$ n'est pas réalisable : il s'agirait de trouver un
+programme qui transforme une solution du 2\textsuperscript{e} problème
+en une solution du 1\textsuperscript{er}.
+
+\medskip
+
+De nouveau, ceci montre que ces formules ne sont pas prouvables.
+
+\medskip
+
+{\footnotesize En revanche, $(A\lor\neg A) \Rightarrow (\neg\neg A
+  \Rightarrow A)$ est réalisable car démontrable : le $\lambda$-terme
+  $\lambda (z:A\lor\neg A). \lambda(u:\neg\neg A).\,
+  (\texttt{match}\ z\ \texttt{with}\ \iota_1 v_1 \mapsto v_1,\;
+  \iota_2 v_2 \mapsto \texttt{exfalso}^{(A)}(u v_2))$ le prouve et
+  explique comment le réaliser.\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La réalisabilité propositionnelle : incomplétude}
+
+La réalisabilité suit tellement près les idées de Curry-Howard qu'on
+pourrait naturellement croire que la réciproque est vraie, que toute
+proposition réalisable donnera un $\lambda$-terme de preuve, i.e., que
+la sémantique est complète.
+
+\medskip
+
+\alert{Surprise : non !}
+
+\medskip
+
+On connaît des formules propositionnelles, p.ex. (transp. suivant) :
+\[
+\begin{aligned}
+&\Big(\neg (A_1 \land A_2) \land (\neg A_1 \Rightarrow (B_1 \lor B_2))
+  \land (\neg A_2 \Rightarrow (B_1 \lor B_2))\Big)\\
+\Rightarrow\,& \Big((\neg A_1 \Rightarrow B_1)\lor(\neg A_2 \Rightarrow B_1)\lor(\neg
+  A_1 \Rightarrow B_2)\lor(\neg A_2 \Rightarrow B_2)\Big)
+\end{aligned}
+\]
+
+\medskip
+
+\textbf{Problèmes ouverts :} l'ensemble des formules réalisables
+est-il décidable ?  Semi-décidable ?
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Réalisabilité de la formule de Tseitin}
+
+{\footnotesize\textcolor{gray}{Ceci est une digression mais je pense
+    que c'est très instructif pour la calculabilité de comprendre la
+    différence entre typage et réalisabilité.}\par}
+
+\smallskip
+
+La formule suivant, bien que non démontrable, est réalisable :
+\[
+\begin{aligned}
+&(\neg (A_1 \land A_2) \land (\neg A_1 \Rightarrow (B_1 \lor B_2))
+  \land (\neg A_2 \Rightarrow (B_1 \lor B_2)))\\
+\Rightarrow\,& ((\neg A_1 \Rightarrow B_1)\lor(\neg A_2 \Rightarrow B_1)\lor(\neg
+  A_1 \Rightarrow B_2)\lor(\neg A_2 \Rightarrow B_2))
+\end{aligned}
+\]
+
+{\footnotesize
+
+\textbf{Algorithme} (appelons $A_1,A_2,B_1,B_2$ les parties
+concernées) :
+
+\smallskip
+
+\itempoint On reçoit en entrée une promesse que l'un de $A_1$ et $A_2$
+est vide, ainsi que deux algorithmes, l'un $e_1 \in (\dottedneg A_1
+\dottedlimp (B_1 \dottedlor B_2))$ prenant en entrée une promesse que
+$A_1=\varnothing$ et renvoyant un élément de $B_1$ ou $B_2$, et
+l'autre $e_2$ prenant en entrée une promesse que $A_2=\varnothing$ et
+renvoyant un élément de $B_1$ ou $B_2$.
+
+\smallskip
+
+\itempoint On \alert{lance en parallèle} $e_1$ resp. $e_2$ sur un
+entier quelconque promettant (peut-être faussement) $A_1=\varnothing$
+resp. $A_2=\varnothing$.  Au moins l'une de ces promesses est vraie
+(par la promesse en entrée) donc l'un de $e_1$ ou $e_2$ va terminer,
+et renvoyer soit un élément annoncé de $B_1$ soit de $B_2$.
+
+\smallskip
+
+Disons sans perte de généralité que $e_1$ renvoie un élément $n$
+annoncé de $B_1$.
+
+\smallskip
+
+\itempoint On renvoie alors comme élément de $\dottedneg A_1
+\dottedlimp B_1$ un programme renvoyant constamment $n$.  Il est bien
+dans l'ensemble annoncé car on a reçu une promesse que
+$A_1=\varnothing$, donc à l'étape précédente le programme a tourné sur
+une vraie promesse et donc a vraiment renvoyé un élément de $B_1$.
+
+\par}
+
+\end{frame}
+%
 % TODO:
 % - inférence de type de Hindley-Milner
 %