From 9709577b7abd152965aef9f17a7aa0cc27661a6d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 12:49:46 +0100
Subject: Comments on negation and double negation.

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

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 3a6a49a..8cc025c 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2417,6 +2417,44 @@ $\Rightarrow$ comme interchangeables.
 
 \par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{La négation et la double négation}
+
+\textcolor{orange}{Qu'est-ce qui correspond à la proposition $\neg P$
+  par Curry-Howard ?}
+
+\medskip
+
+C'est le type $\sigma \rightarrow 0$ des fonctions prenant un argument
+de type $\sigma$ et renvoyant une valeur impossible, i.e., ne peuvent
+jamais renvoyer.
+
+\medskip
+
+Mais on parle d'un langage ($\lambda$CST enrichi) où \alert{tous les
+  programmes terminent} (« normalisation forte ») !  Donc une telle
+fonction prouve que $\sigma$ est lui-même vide ; et la fonction est
+triviale : c'est une « pure preuve » de vacuité de $\sigma$ :
+
+\smallskip
+
+\begin{itemize}
+\item le type $\sigma \rightarrow 0$ (ou « $\neg\sigma$ ») est le type
+  des « témoignages de vacuité » de $\sigma$ \textcolor{teal}{(si on
+    me fournit un truc de type $\sigma$, je soulève une exception
+    parce que c'est impossible)},
+\item le type $(\sigma \rightarrow 0) \rightarrow 0$ (ou
+  « $\neg\neg\sigma$ ») est une sorte de type des témoignages de
+  \alert{non-vacuité} de $\sigma$,
+\item mais ce dernier ne permet pas « magiquement » d'en tirer une
+  valeur :
+\item pas de terme de type $((\alpha \rightarrow 0) \rightarrow 0) \to
+  \alpha$ ou bien $\alpha + (\alpha\rightarrow 0)$ dans le
+  $\lambda$CST : on est bien en \alert{logique intuitionniste}.
+\end{itemize}
+
 \end{frame}
 %
 % TODO:
@@ -2426,6 +2464,8 @@ $\Rightarrow$ comme interchangeables.
 % - présentation en calcul des séquents
 % - élimination des coupures
 % - Kripke
+% - fragment négatif
+% - call/cc
 % - inférence de type de Hindley-Milner
 %
 \end{document}
-- 
cgit v1.2.3