diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 250 |
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 % |