From e792e2a0ff1c0431ec214fdaf72c365765afe3f5 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 13:06:16 +0100
Subject: A start of polymorphism, and substitution for type/prop variables.

---
 transp-inf110-02-typage.tex | 37 +++++++++++++++++++++++++++++++++++--
 1 file changed, 35 insertions(+), 2 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 8cc025c..131e3f2 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2455,11 +2455,44 @@ triviale : c'est une « pure preuve » de vacuité de $\sigma$ :
   $\lambda$CST : on est bien en \alert{logique intuitionniste}.
 \end{itemize}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Un embryon de polymorphisme}
+
+\itempoint Les types du $\lambda$CST sont écrits avec des
+\alert{variables de types} $\alpha,\beta,\gamma$…  En principe ce sont
+des \alert{types opaques}.  En pratique, une fonction comme
+$\lambda(x:\alpha).\lambda(y:\beta).x$ de type
+$\alpha\to\beta\to\alpha$ se comporte \alert{comme polymorphe} : on
+peut imaginer un $\forall\alpha,\beta$ (\alert{implicite}) devant :
+
+\medskip
+
+\itempoint En effet, substituer n'importe quel type $\sigma$ à une
+variable de type $\alpha$ dans un terme du $\lambda$CST (enrichi)
+donne encore un terme correct (la dérivation de typage est la même,
+après substitution).
+
+\medskip
+
+\itempoint Conséquence côté logique : substituer des propositions
+quelconques aux \alert{variables propositionnelles} d'une tautologie
+donne encore une tautologie.
+
+\medskip
+
+P.ex. : $(A\land B\Rightarrow C) \Rightarrow (A\Rightarrow
+B\Rightarrow C)$ est une tautologie, donc
+\[
+((D\Rightarrow E)\land (E\Rightarrow D) \Rightarrow D) \Rightarrow ((D\Rightarrow E)\Rightarrow (E\Rightarrow D)\Rightarrow D)
+\]
+en est une (par substitution de $D\Rightarrow E$ pour $A$, de
+$E\Rightarrow D$ pour $B$, et de $D$ pour $C$).
+
 \end{frame}
 %
 % TODO:
-% - discussion de la négation et double négation
-% - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
 % - présentation en calcul des séquents
 % - élimination des coupures
-- 
cgit v1.2.3