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