Fix various mistakes and make some improvements noted during lecture on 2023-12-19.

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}
 %