From 488414f2691ce8173032316d69060e8f37f9a962 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 15 Nov 2023 12:10:10 +0100
Subject: Curry's paradox (an interlude).

---
 transp-inf110-02-typage.tex | 88 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)

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
@@ -506,6 +506,94 @@ fonctions p.r.
 
 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}
-- 
cgit v1.2.3