diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 82 |
1 files changed, 52 insertions, 30 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 288863d..c5a8f1f 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2491,6 +2491,7 @@ triviale : c'est une « pure preuve » de vacuité de $\sigma$ : \end{frame} % \begin{frame} +\label{variables-are-effectively-polymorphic} \frametitle{Un embryon de polymorphisme} \itempoint Les types du $\lambda$CST sont écrits avec des @@ -4197,8 +4198,8 @@ est vrai soit $B$ est faux » (sens en logique classique) mais bien lorsqu'elle est validée par toute affectation de vérité pour chacune de ses variables (= tout modèle sur ce cadre) ; \item $\varphi$ est \textbf{validée} par \alert{la sémantique de - Kripke} lorsque $\varphi$ est validée par tout cadre (i.e., tout - modèle de Kripke). + Kripke} lorsque $\varphi$ est validée par \alert{tout} cadre (i.e., + tout modèle de Kripke). \end{itemize} \bigskip @@ -4232,38 +4233,47 @@ donné, ils peuvent valider des formules non démontrables. $p_A$ et si $w\geq w'$ ceci contredit la permanence de $p_B$~\qedsymbol)} qui n'est pas prouvable en logique propositionnelle intuitionniste. -\item Le cadre le plus simple après un singleton est $(\{0,1\},\leq)$, - qui correspond à une logique à trois valeurs de vérité, avec les +\item Le cadre le plus simple après un singleton est $\{u,v\}$ avec + $u\leq v$, qui correspond à une logique à 3 valeurs de vérité, aux tableaux suivants. \end{itemize} {\footnotesize -\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c} +\begin{tabular}{c|@{\hskip 15bp}c@{\hskip 15bp}c@{\hskip 15bp}c} +$ +\begin{array}{c|cc} +p&u&v\\\hline +0&0&0\\ +\mathsf{q}&0&1\\ +1&1&1\\ +\end{array} +$ +& $ \begin{array}{c|ccc} -\dottedland&0&?&1\\\hline +\dottedland&0&\mathsf{q}&1\\\hline 0&0&0&0\\ -?&0&?&?\\ -1&0&?&1\\ +\mathsf{q}&0&\mathsf{q}&\mathsf{q}\\ +1&0&\mathsf{q}&1\\ \end{array} $ & $ \begin{array}{c|ccc} -\dottedlor&0&?&1\\\hline -0&0&?&1\\ -?&?&?&1\\ +\dottedlor&0&\mathsf{q}&1\\\hline +0&0&\mathsf{q}&1\\ +\mathsf{q}&\mathsf{q}&\mathsf{q}&1\\ 1&1&1&1\\ \end{array} $ & $ \begin{array}{c|ccc} -A \dottedlimp B&B=0&B={?}&B=1\\\hline +A \dottedlimp B&B=0&B={\mathsf{q}}&B=1\\\hline A=0&1&1&1\\ -A={?}&0&1&1\\ -A=1&0&?&1\\ +A={\mathsf{q}}&0&1&1\\ +A=1&0&\mathsf{q}&1\\ \end{array} $ \end{tabular} @@ -4572,6 +4582,16 @@ On connaît des formules propositionnelles, p.ex. (transp. suivant) : A_1 \Rightarrow B_2)\lor(\neg A_2 \Rightarrow B_2)\Big) \end{aligned} \] +qui sont réalisables mais non prouvables en logique intuitionniste. + +\smallskip + +{\footnotesize C'est-à-dire que bien qu'on ait un algorithme + (transp. suivant) qui réalise cette formule pour toutes parties + $A_1,A_2,B_1,B_2$ de $\mathbb{N}$ (et moralement : toutes données), + on ne peut pas typer un tel algorithme, lequel dépend de la + possibilité de faire temporairement des « fausses promesses » pour + donner finalement un résultat juste.\par} \medskip @@ -4610,16 +4630,17 @@ concernées) : est vide, ainsi que deux algorithmes, l'un $e_1 \in (\dottedneg A_1 \dottedlimp (B_1 \dottedlor B_2))$ prenant en entrée une promesse que $A_1=\varnothing$ et renvoyant un élément de $B_1$ ou $B_2$, et -l'autre $e_2$ prenant en entrée une promesse que $A_2=\varnothing$ et -renvoyant un élément de $B_1$ ou $B_2$. +l'autre $e_2$ prennant promesse $A_2=\varnothing$ et renvoyant un +él\textsuperscript{t} de $B_1$ ou $B_2$. \smallskip \itempoint On \alert{lance en parallèle} $e_1$ resp. $e_2$ sur un -entier quelconque promettant (peut-être faussement) $A_1=\varnothing$ -resp. $A_2=\varnothing$. Au moins l'une de ces promesses est vraie -(par la promesse en entrée) donc l'un de $e_1$ ou $e_2$ va terminer, -et renvoyer soit un élément annoncé de $B_1$ soit de $B_2$. +entier qcque promettant (peut-être faussement !) +$A_1=\varnothing$ resp. $A_2=\varnothing$. Au moins l'une de ces +promesses est vraie (par la promesse en entrée) donc l'un de $e_1$ ou +$e_2$ va terminer, et renvoyer soit un élément annoncé de $B_1$ soit +de $B_2$. \smallskip @@ -4630,9 +4651,9 @@ annoncé de $B_1$. \itempoint On renvoie alors comme élément de $\dottedneg A_1 \dottedlimp B_1$ un programme renvoyant constamment $n$. Il est bien -dans l'ensemble annoncé car on a reçu une promesse que -$A_1=\varnothing$, donc à l'étape précédente le programme a tourné sur -une vraie promesse et donc a vraiment renvoyé un élément de $B_1$. +dans $\dottedneg A_1 \dottedlimp B_1$ car s'il reçoit une promesse que +$A_1=\varnothing$, à l'étape précédente le programme a tourné sur une +vraie promesse et donc a vraiment renvoyé un élément de $B_1$. \par} @@ -4900,10 +4921,10 @@ reste des contraintes : \begin{itemize} \item si $\zeta_1 = \zeta_2$ déjà, unifier $\mathscr{C}'$, \item si $\zeta_1$ est une \alert{variable} de type $\eta$ : - \alert{si} $\zeta_2$ ne fait pas intervenir $\eta$, ajouter $\eta - \mapsto \zeta_2$ à la substitution, et unifier $\mathscr{C}'$ où - $\eta$ est remplacé par $\zeta_2$ ; \alert{sinon}, \alert{échouer} - (« type récursif ») ; + \alert{si} $\zeta_2$ ne fait pas intervenir $\eta$, ajouter (et + appliquer) $\eta \mapsto \zeta_2$ à la substitution, et unifier + $\mathscr{C}'$ où $\eta$ est remplacé par $\zeta_2$ ; \alert{sinon}, + \alert{échouer} (« type récursif ») ; \item si $\zeta_2$ est une variable de type : symétriquement ; \item sinon, $\zeta_1 = (\xi_1 \to \chi_1)$ et $\zeta_2 = (\xi_2 \to \chi_2)$ : unifier $\mathscr{C}'' := \mathscr{C}' \cup \{(\xi_1 = @@ -5069,9 +5090,10 @@ let twice = fun f -> fun x -> f(f x) in (twice ((+)1) 42, twice not true) ;;\\ \itempoint Pour réparer ce problème, très grossièrement : \textcolor{blue}{(a)} on type d'abord $x$, puis \textcolor{blue}{(b)} on « \alert{généralise} » chaque variable de -type (non présente dans le contexte d'ensemble), c'est-à-dire que -\textcolor{blue}{(c)} chaque apparition de $v$ dans $t$ reçoit des -variables de type fraîches à ces places (ce qui le rend polymorphe). +type (non présente dans le contexte d'ensemble) pour rendre $x$ +polymorphe (cf. \ref{variables-are-effectively-polymorphic}), +c'est-à-dire que \textcolor{blue}{(c)} \alert{chaque} apparition de +$v$ dans $t$ reçoit des variables de type fraîches à ces places. \end{frame} % |