From 9709577b7abd152965aef9f17a7aa0cc27661a6d Mon Sep 17 00:00:00 2001 From: "David A. Madore" 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(+) (limited to 'transp-inf110-02-typage.tex') 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