diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 37 |
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 |