summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-02-typage.tex88
1 files changed, 88 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index f84f192..60bef3a 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -508,4 +508,92 @@ Exemple de tel langage : Coq.
\end{frame}
%
+\begin{frame}
+\frametitle{La correspondance de Curry-Howard (avant-goût)}
+
+Idée générale : établir une analogie, voire une correspondance précise
+entre
+\begin{itemize}
+\item \textbf{types} et \textbf{termes} de ces types dans un système
+ de typage,
+\item \textbf{propositions} et \textbf{preuves} de ces propositions
+ dans un système logique.
+\end{itemize}
+
+\smallskip
+
+P.ex., la preuve évidente de l'affirmation $(A \land B) \Rightarrow A$
+(« si $A$ et $B$ sont vraies alors $A$ est vraie ») correspond à la
+« première projection » de type $a \times b \rightarrow a$.
+
+\smallskip
+
+{\footnotesize Ceci « explique » que le type d'un terme tel que
+ $\lambda xy.x$, soit $u \to v \to u$, soit une vérité logique, en
+ l'occurrence $U \Rightarrow V \Rightarrow U$ (« si $U$ est vrai
+ alors, si $V$ est vrai alors $U$ est vrai »).\par}
+
+\bigskip
+
+Beaucoup de variations sur cette correspondance, mais il y a des
+restrictions :
+\begin{itemize}
+\item le langage informatique doit garantir la terminaison, sinon cela
+ reviendrait à permettre les preuves circulaires,
+\item la logique concernée est plutôt « intuitionniste » (sans tiers
+ exclu),
+\item diverses subtilités notamment dans la correspondance entre types
+ sommes paramétriques et $\exists$ côté logique.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Paradoxe de Curry (interlude distrayant)}
+
+{\footnotesize Variante plus sophistiquée de « cette phrase est
+ fausse ». C'est un exemple de preuve circulaire
+ ($\leftrightarrow$ combinateur $\mathsf{Y}$ de Curry par la
+ correspondance de C-H), invalide en logique.\par}
+
+\medskip
+
+Je tiens l'affirmation : « \textcolor{teal}{si j'ai raison, alors je
+ suis un grand génie} ».
+
+\begin{itemize}
+\item clairement, si j'ai raison, je suis un grand génie ;
+\item mais c'était justement mon affirmation : donc j'ai raison ;
+\item donc je suis un grand génie. \qedsymbol
+\end{itemize}
+
+{\footnotesize Remplacer « j'ai raison » par « cette phrase est
+ vraie » (voire utiliser l'astuce de Quine pour éviter « cette
+ phrase ») et « je suis un grand génie » par absolument n'importe
+ quoi.\par}
+
+\bigskip
+
+\itempoint Ce qui est correct : \alert{si on peut construire} un
+énoncé $A$ tel que $A \Leftrightarrow (A \Rightarrow B)$ (ici $A$ est
+l'affirmation tenue et $B$ est la conclusion voulue) alors $B$ vaut :
+\[
+(A \Leftrightarrow (A \Rightarrow B)) \, \Rightarrow \, B
+\]
+
+{\footnotesize (Preuve correcte : supposons $A$ : par hypothèse, ceci
+ signifie $A \Rightarrow B$ ; on a donc $B$ ; tout ceci prouve $A
+ \Rightarrow B$. Bref on a $A \Rightarrow B$. Mais par hypothèse
+ c'est $A$. Donc $A$ vaut. Donc $B$ aussi.)\par}
+
+\medskip
+
+\itempoint Ce qui est \textcolor{orange}{fallacieux} : la supposition
+tacite qu'on peut construire un tel $A$.
+
+{\footnotesize L'astuce de Quine permet de faire une auto-référence
+ sur la syntaxe, pas sur la vérité.\par}
+
+\end{frame}
+%
\end{document}