From 209d70fc8229cbb320c39489111c5ece8801d5e6 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 19 Dec 2023 10:18:59 +0100
Subject: Add a slide on impredicativity.

---
 transp-inf110-03-super.tex | 52 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

(limited to 'transp-inf110-03-super.tex')

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index 76edb90..1201c29 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -223,6 +223,58 @@ $x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
   (Les détails dépendent du système logique précis considéré {\tiny et
     si Martin-Löf est dans la salle}.)}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Imprédicativité}
+
+\itempoint On appelle \textbf{imprédicativité} la possibilité de
+définir une proposition ou un type en quantifiant sur toutes les
+propositions ou types \alert{y compris celui qu'on définit} : c'est
+une forme de circularité.
+
+\medskip
+
+\itempoint P.ex., $\forall (Z:*).\, (Z \Rightarrow A)$ représente le
+type des fonctions capables de renvoyer un type $A$ à partir d'un type
+$Z$ quelconque, y compris celui qu'on définit.
+
+\smallskip
+
+Cette imprédicativité est utile pour définir des constructions sur les
+types.
+
+\medskip
+
+{\footnotesize
+
+Exemples (informellement, et en notant « $*$ » le « type des types »
+imprédicatif) :
+\begin{itemize}
+\item $A \; \cong \; \forall (Z:*).\, (Z \Rightarrow A)$ : donné une
+  valeur $x$ de type $A$ on peut en fabriquer une de type
+  $Z\Rightarrow A$ comme $\lambda(z:Z).\, x$ pour tout type $Z$, mais
+  réciproquement, donné une valeur de type $\forall (Z:*).\, (Z
+  \Rightarrow A)$ on peut l'appliquer à $Z = \top$ pour obtenir une
+  valeur de type $A$.
+\item $A \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z) \Rightarrow
+  Z)$ : dans un sens on fabrique $\lambda(k:A \Rightarrow Z).\, kx$
+  comme pour le CPS, dans l'autre sens, appliquer à $Z = A$ et
+  l'identité.
+\item $\bot \; \cong \; \forall (Z:*).\, Z$
+\quad\itempoint $A\land B \; \cong \; \forall (Z:*).\, ((A \Rightarrow B
+  \Rightarrow Z) \Rightarrow Z)$
+\item $A\lor B \; \cong \; \forall (Z:*).\, ((A \Rightarrow Z)
+  \Rightarrow (B\Rightarrow Z) \Rightarrow Z)$
+\end{itemize}
+
+\par}
+
+\medskip
+
+\itempoint Cela \alert{peut} donner des incohérences logiques
+(paradoxe de Girard).
+
 \end{frame}
 %
 \section{Logique du premier ordre}
-- 
cgit v1.2.3