diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 185 |
1 files changed, 162 insertions, 23 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 0ef600c..b16fb58 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -93,9 +93,11 @@ 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(v)$ dépendant d'une variable $v$ libre, -\item lient cette variable pour former une nouvelle formule $\forall - v. P(v)$ ou $\exists v. P(v)$. +\item prennent une formule $P(v)$ dépendant d'une variable $v$ libre + {\footnotesize (de type $I$)}, +\item lient cette variable, pour former une nouvelle formule : + $\forall (v:I). P(v)$ ou $\exists (v:I). P(v)$ + {\footnotesize (parfois juste $\forall v. P(v)$ et $\exists v. P(v)$)}. \end{itemize} \medskip @@ -113,7 +115,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 -$v$ ici ? quel est leur domaine ?). +$v$ ici ? quel est leur domaine $I$ ?). \smallskip @@ -137,10 +139,10 @@ maintenant les quantificateurs : de transformer un témoignage de $P$ en un témoignage de $Q$,} \item {\color{darkgray} un témoignage de $\top$ est trivial,} \quad \itempoint {\color{darkgray} un témoignage de $\bot$ n'existe pas,} -\item un témoignage de $\forall x.P(x)$ est un moyen +\item un témoignage de $\forall v.P(v)$ est un moyen de transformer un $x$ quelconque en un témoignage de $P(x)$, -\item un témoignage de $\exists x.P(x)$ est la donnée d'un certain - $x_0$ et d'un témoignage de $P(x_0)$. +\item un témoignage de $\exists v.P(v)$ est la donnée d'un certain + $t_0$ et d'un témoignage de $P(t_0)$. \end{itemize} \end{frame} @@ -170,16 +172,17 @@ prendre le produit. \medskip -\itempoint Une preuve de $\forall v.P(v)$ correspondra à un terme de -forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond -à $P(v)$. +\itempoint Une preuve de $\forall (v:I).P(v)$ correspondra à un terme +de forme $\lambda(v:I).\,(\cdots)$, où le type de $(\cdots)$ +correspond à $P(v)$. \medskip -\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} S = S^I$ (ensemblistement ou numériquement). {\footnotesize (Les - détails dépendent de la nature de la quantification.)} +\itempoint Remarquer que $\forall (v:I).P$, si $P$ ne dépend pas de +$v$, « ressemble » à $I \Rightarrow P$ de la même manière que +$\prod_{i\in I} S = S^I$ (ensemblistement ou numériquement). + {\footnotesize (Les détails dépendent de la nature de la + quantification.)} \end{frame} % @@ -195,22 +198,22 @@ forme $\lambda(v:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond \medskip \itempoint De façon analogue, la \alert{quantification existentielle} -$\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 +$\exists v. P(v)$ {\footnotesize (« la donnée d'un $t_0$ et d'un + témoignage de $P(t_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)$ »)}. + famille} $\sum_v \sigma(v)$ {\footnotesize (« donnée d'un $t_0$ et + d'une valeur de type $\sigma(t_0)$ »)}. \medskip -\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 +\itempoint Une preuve de $\exists (v:I).P(v)$ correspondra à un terme de +forme $\langle t_0, \cdots\rangle$, où le type de $(\cdots)$ +correspond à $P(t_0)$. {\footnotesize (De nouveau, il faut des « familles de types ».)} \medskip -\itempoint Remarquer que $\exists v.P$, si $P$ ne dépend pas de $v$, +\itempoint Remarquer que $\exists (v:I).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.)} @@ -219,13 +222,149 @@ I\times S$. {\footnotesize (Les détails dépendent de la nature de la \itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit que d'une preuve de $\exists v.P(v)$ on \alert{puisse extraire} le -$v_0$ correspondant dans autre chose qu'une preuve. {\footnotesize +$t_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}.)} \end{frame} % \begin{frame} +\frametitle{Règles d'introduction et d'élimination de $\forall$} + +{\footnotesize\textcolor{orange}{Les règles ci-dessous (et + transp. suivant) sont \alert{incomplètes} : il manque des + explications sur le type $I$ sur lequel on quantifie et comment on + peut en former des « termes ».}\par} + +\medskip + +\itempoint \underline{Introduction du $\forall$ :} pour montrer +$\forall (v:I).\, Q$, on s'arrange (quitte à renommer la variable +liée) pour que $v:I$ soit « frais », c'est-à-dire qu'il n'apparaisse +(libre) dans \alert{aucune hypothèse} en cours : si on montre $Q$ sur +ce $v$ « arbitraire », on peut conclure $\forall (v:I).\, Q$. + +\smallskip + +{\footnotesize (Rédaction : « soit $v$ arbitraire (…) on a $Q(v)$ ; + donc $\forall (v:I).\, Q(v)$ ».)\par} + +\medskip + +\textcolor{teal}{Ceci donnera un $\lambda$-terme noté + $\lambda(v:I).(\cdots)$ comme l'ouverture d'une hypothèse.} + +\bigskip + +\itempoint \underline{Élimination du $\forall$ :} pour utiliser +$\forall (v:I). Q$, on peut l'appliquer à un $t$ quelconque (un +\alert{terme} de type $I$). + +\smallskip + +{\footnotesize (Rédaction : « on a $\forall (v:I). Q(v)$ et $t$ de + type $I$ ; en particulier, on a $Q(t)$ ».)\par} + +\medskip + +\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $ft$ comme + l'application d'une implication.} + +\end{frame} +% +\begin{frame} +\frametitle{Règles d'introduction et d'élimination de $\exists$} + +\itempoint \underline{Introduction du $\exists$ :} pour montrer +$\exists (v:I). Q$, on peut le montrer sur un terme $t$ quelconque de +type $I$. + +\smallskip + +{\footnotesize (Rédaction : « pour ce $t$ de type $I$ on a $Q(t)$ ; en + particulier, on a $\exists (v:I). Q(v)$ ».)\par} + +\medskip + +\textcolor{teal}{Ceci donnera un $\lambda$-terme noté $\langle + t,\cdots\rangle$ comme pour une conjonction.} + +\bigskip + +\itempoint \underline{Élimination du $\exists$ :} pour utiliser +$\exists (v:I). P(v)$ pour montrer une conclusion $Q$, on s'arrange +(quitte à renommer la variable liée) pour que $v$ soit « frais », +c'est-à-dire qu'il n'apparaisse (libre) dans \alert{aucune hypothèse} +en cours \alert{ni dans la conclusion} $Q$ : si on montre $Q$ à partir +de $P$ sur ce $v$ « arbitraire », on peut conclure $Q$ à partir de +$\exists v. P$. + +\smallskip + +{\footnotesize (Rédaction : « on a $\exists (v:I). P(v)$ : soit $v$ + arbitraire tel que $P(v)$ : (…) on a $Q$ ; donc $Q$ ».)\par} + +\medskip + +\textcolor{teal}{Ceci donnera un $\lambda$-terme noté + $(\texttt{match~}\cdots\texttt{~with~}\langle v,h\rangle \mapsto + \cdots)$.} + +\end{frame} +% +\begin{frame} +\frametitle{Aperçu d'ensemble des règles de la déduction naturelle} + +\begin{tabular}{c|c|c} +&Intro&Élim\\\hline +$\Rightarrow$ +&\scalebox{0.65}{$\inferrule{\Gamma,{\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash P\Rightarrow Q}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$} +\\\hline +$\land$ +&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$} +\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$} +\\\hline +$\lor$ +&\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$} +\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash P_1\lor P_2\\\Gamma,{\color{mydarkgreen}P_1}\vdash Q\\\Gamma,{\color{mydarkgreen}P_2}\vdash Q}{\Gamma\vdash Q}$} +\\\hline +$\top$ +&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \top}$} +&\scalebox{0.65}{(néant)} +\\\hline +$\bot$ +&\scalebox{0.65}{(néant)} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash \bot}{\Gamma\vdash Q}$ +(ou pour la logique classique : $\inferrule{\Gamma,\neg Q\vdash \bot}{\Gamma\vdash Q}$)} +\\\hline +$\forall$ +&$\inferrule{\Gamma, {\color{mydarkgreen}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais}) +&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$ +\\\hline +$\exists$ +&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$ +&$\inferrule{\Gamma\vdash \exists (v:I). P\\\Gamma, {\color{mydarkgreen}v:I}, {\color{mydarkgreen}P}\vdash Q}{\Gamma\vdash Q}$ +($v$ \alert{frais}) +\\ +\end{tabular} + +\smallskip + +\itempoint « $v$ frais » = « $v$ n'apparaît nulle part ailleurs » +(cf. transp. précédents). + +\smallskip + +\itempoint Le contexte $\Gamma$ peut contenir des formules +(hypothèses) et des variables d'« individus » (avec leur type, +p.ex. $v:I$). + +\end{frame} +% +\begin{frame} \frametitle{Le problème du $\exists$ et des types sommes} Doit-on croire à ceci (pour $U$ et $V$ deux types) ? |