diff options
author | David A. Madore <david+git@madore.org> | 2023-12-04 12:49:46 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-12-04 12:49:46 +0100 |
commit | 9709577b7abd152965aef9f17a7aa0cc27661a6d (patch) | |
tree | b0b93e111bdd3f63fd14e2120187fc49f2b08f78 /transp-inf110-02-typage.tex | |
parent | e0c714d1e5e035db928f07f740ba4cc1ed64707a (diff) | |
download | inf110-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.tex | 40 |
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} |