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

2 files changed, 85 insertions, 63 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}
 %
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 0626337..0ef600c 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -93,9 +93,9 @@ connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$.
 mathématiques au-delà de ces connecteurs : les
 \textbf{quantificateurs} $\forall,\exists$, qui :
 \begin{itemize}
-\item prennent une formule $P(x)$ dépendant d'une variable $x$ libre,
+\item prennent une formule $P(v)$ dépendant d'une variable $v$ libre,
 \item lient cette variable pour former une nouvelle formule $\forall
-  x. P(x)$ ou $\exists x. P(x)$.
+  v. P(v)$ ou $\exists v. P(v)$.
 \end{itemize}
 
 \medskip
@@ -103,9 +103,9 @@ mathématiques au-delà de ces connecteurs : les
 \itempoint Intuitivement, il faut penser à $\forall$ et $\exists$
 comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
 \begin{itemize}
-\item $\forall x.P(x)$, parfois noté $\bigwedge_x P(x)$ est à $P\land
+\item $\forall v.P(v)$, parfois noté $\bigwedge_v P(v)$ est à $P\land
   Q$ ce que $\prod_i p_i$ est à $p\times q$,
-\item $\exists x.P(x)$, parfois noté $\bigvee_x P(x)$ est à $P\lor Q$
+\item $\exists v.P(v)$, parfois noté $\bigvee_v P(v)$ est à $P\lor Q$
   ce que $\sum_i p_i$ est à $p + q$.
 \end{itemize}
 
@@ -113,7 +113,7 @@ comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
 
 \itempoint Il existe de \alert{nombreux systèmes logiques} différant
 notamment en \alert{ce qu'on a le droit de quantifier} (qui sont les
-$x$ ici ?).
+$v$ ici ? quel est leur domaine ?).
 
 \smallskip
 
@@ -156,30 +156,30 @@ maintenant les quantificateurs :
 \medskip
 
 \itempoint De façon analogue, la \alert{quantification universelle}
-$\forall x. P(x)$ {\footnotesize (« une façon de transformer $x$ en un
-  témoignage de $P(x)$ »)}, qui est une sorte de \emph{conjonction en
-famille} $\bigwedge_x P(x)$, correspondra au \alert{type produit en
-  famille} $\prod_x \sigma(x)$ {\footnotesize (« fonction renvoyant
-  une valeur de $\sigma(x)$ pour chaque $x$ »)}.
+$\forall v. P(v)$ {\footnotesize (« une façon de transformer $v$ en un
+  témoignage de $P(v)$ »)}, qui est une sorte de \emph{conjonction en
+famille} $\bigwedge_v P(v)$, correspondra au \alert{type produit en
+  famille} $\prod_v \sigma(v)$ {\footnotesize (« fonction renvoyant
+  une valeur de $\sigma(v)$ pour chaque $v$ »)}.
 
 \medskip
 
-\itempoint Ceci présuppose l'existence de \alert{familles de types} $x
-\mapsto \sigma(x)$ (= types dépendant de quelque chose) dont on puisse
+\itempoint Ceci présuppose l'existence de \alert{familles de types} $v
+\mapsto \sigma(v)$ (= types dépendant de quelque chose) dont on puisse
 prendre le produit.
 
 \medskip
 
-\itempoint Une preuve de $\forall x.P(x)$ correspondra à un terme de
-forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
-à $P(x)$.
+\itempoint Une preuve de $\forall v.P(v)$ correspondra à un terme de
+forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
+à $P(v)$.
 
 \medskip
 
-\itempoint Remarquer que $\forall x.P$, si $P$ ne dépend pas de $x$,
+\itempoint Remarquer que $\forall v.P$, si $P$ ne dépend pas de $v$,
 « ressemble » à $I \Rightarrow P$ de la même manière que $\prod_{i\in
-  I} X = X^I$.  {\footnotesize (Les détails dépendent de la nature de
-  la quantification.)}
+  I} S = S^I$ (ensemblistement ou numériquement).  {\footnotesize (Les
+  détails dépendent de la nature de la quantification.)}
 
 \end{frame}
 %
@@ -187,7 +187,7 @@ forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
 \frametitle{Curry-Howard pour le $\exists$}
 
 \itempoint On a vu que Curry-Howard fait correspondre
-\alert{conjonction logique} $P\lor Q$ {\footnotesize (« un témoignage
+\alert{disjonction logique} $P\lor Q$ {\footnotesize (« un témoignage
   de $P$ ou un de $Q$, avec la donnée duquel on a choisi »)} avec
 \alert{type somme} $\sigma+\tau$ {\footnotesize (« une valeur de
   $\sigma$ ou une de $\tau$, avec un sélecteur entre les deux »)}.
@@ -195,31 +195,31 @@ forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
 \medskip
 
 \itempoint De façon analogue, la \alert{quantification existentielle}
-$\exists x. P(x)$ {\footnotesize (« la donnée d'un $x_0$ et d'un
-  témoignage de $P(x_0)$ »)}, qui est une sorte de \emph{disjonction
-en famille} $\bigvee_x P(x)$, correspondra au \alert{type somme en
-  famille} $\sum_x \sigma(x)$ {\footnotesize (« donnée d'un $x_0$ et
-  d'une valeur de type $\sigma(x_0)$ »)}.
+$\exists v. P(v)$ {\footnotesize (« la donnée d'un $v_0$ et d'un
+  témoignage de $P(v_0)$ »)}, qui est une sorte de \emph{disjonction
+en famille} $\bigvee_v P(v)$, correspondra au \alert{type somme en
+  famille} $\sum_v \sigma(v)$ {\footnotesize (« donnée d'un $v_0$ et
+  d'une valeur de type $\sigma(v_0)$ »)}.
 
 \medskip
 
-\itempoint Une preuve de $\exists x.P(x)$ correspondra à un terme de
-forme $\langle x_0, \cdots\rangle$, où le type de $(\cdots)$
-correspond à $P(x_0)$.  {\footnotesize (De nouveau, il faut des
+\itempoint Une preuve de $\exists v.P(v)$ correspondra à un terme de
+forme $\langle v_0, \cdots\rangle$, où le type de $(\cdots)$
+correspond à $P(v_0)$.  {\footnotesize (De nouveau, il faut des
   « familles de types ».)}
 
 \medskip
 
-\itempoint Remarquer que $\exists x.P$, si $P$ ne dépend pas de $x$,
-« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} X =
-I\times X$.  {\footnotesize (Les détails dépendent de la nature de la
+\itempoint Remarquer que $\exists v.P$, si $P$ ne dépend pas de $v$,
+« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} S =
+I\times S$.  {\footnotesize (Les détails dépendent de la nature de la
   quantification.)}
 
 \medskip
 
 \itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit
-que d'une preuve de $\exists x.P(x)$ on \alert{puisse extraire} le
-$x_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
+que d'une preuve de $\exists v.P(v)$ on \alert{puisse extraire} le
+$v_0$ correspondant dans autre chose qu'une preuve.  {\footnotesize
   (Les détails dépendent du système logique précis considéré {\tiny et
     si Martin-Löf est dans la salle}.)}
 
@@ -263,7 +263,7 @@ fonction.
 Coq (où l'énoncé ci-dessus ne sera pas prouvable pour $P : U\times V
 \to \mathit{Prop}$) et les systèmes à la Martin-Löf comme Agda (où
 Curry-Howard est suivi « jusqu'au bout » : il n'y a pas de $\exists$
-uniquement logique).
+uniquement logique, et cet énoncé est prouvable).
 
 \end{frame}
 %