From 3c06b7f7286175e089f4724d6c003b770f89bd7d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 20 Dec 2023 08:28:07 +0100
Subject: Fix various mistakes and make some improvements noted during lecture
on 2023-12-19.
---
transp-inf110-02-typage.tex | 82 ++++++++++++++++++++++++++++----------------
transp-inf110-03-quantif.tex | 66 +++++++++++++++++------------------
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}
%
--
cgit v1.2.3