An exercise on Curry-Howard.

1 files changed, 109 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 7b163fd..14cf4cf 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1704,6 +1704,115 @@ la portée de définition de la fonction dans un langage fonctionnel.
 \end{corrige}
 
 
+%
+%
+%
+
+\section{Correspondance de Curry-Howard}
+
+
+\exercice\ (${\star}{\star}$)\par\nobreak
+
+Pour chacune des preuves suivantes écrites informellement en langage
+naturel dans le calcul propositionnel, écrire le $\lambda$-terme de
+preuve (c'est-à-dire le terme du $\lambda$-calcul propositionnel
+simplement typé étendu d'un type $\bot$ ayant pour type la proposition
+prouvée) qui lui correspond.  Ces raisonnements sont-ils
+intuitionnistement valables ?  Qu'en conclut-on ?
+
+\textbf{(a)} On va prouver $\neg\neg(A\Rightarrow B) \Rightarrow
+\neg\neg A\Rightarrow\neg\neg B$.  Pour cela, supposons
+$\neg\neg(A\Rightarrow B)$ et $\neg\neg A$ et $\neg B$ et on veut
+arriver à une contradiction.  Supposons $A\Rightarrow B$.  Alors si on
+a $A$, on a $B$, ce qui contredit $\neg B$ ; donc $\neg A$ : mais ceci
+contredit $\neg\neg A$.  Donc $\neg(A\Rightarrow B)$.  Mais ceci
+contredit $\neg\neg(A\Rightarrow B)$, comme annoncé.
+
+\textbf{(b)} On va prouver $(A\Rightarrow\neg\neg B) \Rightarrow
+\neg\neg(A\Rightarrow B)$.  Supposons $A\Rightarrow\neg\neg B$ ainsi
+que $\neg(A\Rightarrow B)$ et on veut arriver à une contradiction.  Si
+on a $B$, alors certainement $A\Rightarrow B$, ce qui contredit
+$\neg(A\Rightarrow B)$ : ceci montre $\neg B$.  Si on a $A$, alors
+notre hypothèse $A\Rightarrow\neg\neg B$ nous donne $\neg\neg B$, d'où
+une contradiction, et notamment $B$.  On a donc prouvé $A\Rightarrow
+B$, d'où la contradiction recherchée.
+
+\textbf{(c)} On va prouver $(\neg\neg A\Rightarrow\neg\neg B)
+\Rightarrow (A\Rightarrow\neg\neg B)$.  Mais on sait que $A$ implique
+$\neg\neg A$, donc $\neg\neg A \Rightarrow C$ implique $A\Rightarrow
+C$ (quel que soit $C$, et notamment pour $\neg\neg B$).
+
+\begin{corrige}
+\textbf{(a)} On commence par se placer avec $f_1:\neg\neg(A\Rightarrow
+B)$ et $x_1:\neg\neg A$ et $k:\neg B$ dans le contexte.  Appelons
+encore $f_0$ l'hypothèse $A\Rightarrow B$.  Le raisonnement « si on a
+$A$, on a $B$, ce qui contredit $\neg B$ » se formalise par le
+$\lambda$-terme $\lambda(x_0:A). k(f_0 x_0)$ de type $\neg A$ ; le
+« mais ceci contredit $\neg\neg A$ » s'obtient en lui appliquant
+$x_1$.  Le $\lambda$-terme $\lambda(f_0:A\Rightarrow B).\,
+x_1(\lambda(x_0:A). k(f_0 x_0))$ est donc de type $\neg(A\Rightarrow
+B)$, et la contradiction avec $\neg\neg(A\Rightarrow B)$ s'exprime en
+lui appliquant $f_1$.  Finalement, le $\lambda$-terme tout entier (de
+type $\neg\neg(A\Rightarrow B) \Rightarrow \neg\neg
+A\Rightarrow\neg\neg B$) est :
+\[
+\lambda(f_1:\neg\neg(A\Rightarrow B)).\,
+\lambda(x_1:\neg\neg A).\,\lambda(k:\neg B).\,
+f_1(\lambda(f_0:A\Rightarrow B).\,
+x_1(\lambda(x_0:A). k(f_0 x_0)))
+\]
+(ou en syntaxe Coq : \texttt{fun (f1 : \textasciitilde
+  \textasciitilde(A->B)) (x1 : \textasciitilde\textasciitilde A) (k :
+  \textasciitilde B) => f1 (fun f0 : A -> B => x1 (fun x0 : A => k (f0
+  x0)))}).
+
+\textbf{(b)} On commence par se placer avec $f_1:A\Rightarrow \neg\neg
+B$ et $k:\neg(A\Rightarrow B)$ dans le contexte.  Appelons $y$
+l'hypothèse $B$ : alors $\lambda(z:A).y$ est de type $A\Rightarrow B$,
+donc $k(\lambda(z:A).y)$ est de type $\bot$, ainsi
+$\lambda(y:B).k(\lambda(z:A).y)$ est de type $\neg B$.  Appelons $x$
+l'hypothèse $A$ : alors $f_1 x$ montre $\neg\neg B$, donc en
+l'appliquant au $\lambda$-terme $\lambda(y:B).k(\lambda(z:A).y)$
+précédemment trouvé on trouve une contradiction, et
+$\texttt{exfalso}^{(B)}(f_1 x \, \lambda(y:B).k(\lambda(z:A).y))$ est
+de type $B$.  En abstrayant $x$ dans ce terme on a un terme de type
+$A\Rightarrow B$, et en lui appliquant $k$ on a la contradiction
+recherchée.  Finalement, le $\lambda$-terme tout entier (de type
+$(A\Rightarrow\neg\neg B) \Rightarrow \neg\neg(A\Rightarrow B)$) est :
+\[
+\lambda(f_1:A\Rightarrow \neg\neg B).\,
+\lambda(k:\neg(A\Rightarrow B)).\,
+k(\lambda(x:A).\,\texttt{exfalso}^{(B)}(f_1 x \, \lambda(y:B).k(\lambda(z:A).y)))
+\]
+(ou en syntaxe Coq : \texttt{fun (f1 : A -> \textasciitilde
+  \textasciitilde B) (k : \textasciitilde (A->B)) => k (fun x : A =>
+  False\_ind B (f1 x (fun y : B => k (fun z : A => y))))}).
+
+\textbf{(c)} La preuve de $A \Rightarrow \neg\neg A$ s'écrit
+$\lambda(x:A).\lambda(k:\neg A).kx$.  La preuve de $A\Rightarrow C$ à
+partir de $\neg\neg A \Rightarrow C$ s'obtient en composant avec cette
+fonction, donc finalement le $\lambda$-terme tout entier (de type
+$(\neg\neg A\Rightarrow\neg\neg B) \Rightarrow (A\Rightarrow\neg\neg
+B)$) est :
+\[
+\lambda(f_1:\neg\neg A\Rightarrow \neg\neg B).\,
+\lambda(x:A).f_1(\lambda(k:\neg A).kx)
+\]
+(ou en syntaxe Coq : \texttt{fun (f1 : \textasciitilde\textasciitilde
+  A -> \textasciitilde\textasciitilde B) (x : A) => f1 (fun k :
+  \textasciitilde A => k x)}).
+
+Les trois raisonnements sont parfaitement valables intuitionnistement
+(malgré les nombreux « supposons (...), contradiction », il s'agit à
+chaque fois de \emph{preuves de négation} et pas de \emph{preuves par
+l'absurde}) : le fait qu'on ait trouvé des $\lambda$-termes (sans
+aucun call/cc dedans) de ces types le montre.
+
+On peut retenir la conclusion que $\neg\neg(A\Rightarrow B)$,
+$\neg\neg A\Rightarrow\neg\neg B$ et $A\Rightarrow\neg\neg B$ sont
+tous les trois équivalents (en logique intuitionniste).
+\end{corrige}
+
 
 %
 %