A start of polymorphism, and substitution for type/prop variables.

1 files 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
@@ -2457,9 +2457,42 @@ triviale : c'est une « pure preuve » de vacuité de $\sigma$ :
 
 \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