diff options
Diffstat (limited to 'transp-inf110-03-quantif.tex')
| -rw-r--r-- | transp-inf110-03-quantif.tex | 66 |
1 files changed, 33 insertions, 33 deletions
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} % |