summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-04 12:49:46 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-04 12:49:46 +0100
commit9709577b7abd152965aef9f17a7aa0cc27661a6d (patch)
treeb0b93e111bdd3f63fd14e2120187fc49f2b08f78 /transp-inf110-02-typage.tex
parente0c714d1e5e035db928f07f740ba4cc1ed64707a (diff)
downloadinf110-lfi-9709577b7abd152965aef9f17a7aa0cc27661a6d.tar.gz
inf110-lfi-9709577b7abd152965aef9f17a7aa0cc27661a6d.tar.bz2
inf110-lfi-9709577b7abd152965aef9f17a7aa0cc27661a6d.zip
Comments on negation and double negation.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex40
1 files changed, 40 insertions, 0 deletions
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
@@ -2419,6 +2419,44 @@ $\Rightarrow$ comme interchangeables.
\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:
% - discussion de la négation et double négation
% - substitution des variables propositionnelles par des formules
@@ -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}