diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 157 |
1 files changed, 156 insertions, 1 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index b16fb58..867d04d 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -313,6 +313,7 @@ $\exists v. P$. \end{frame} % \begin{frame} +\label{natural-deduction-rules-with-quantifiers} \frametitle{Aperçu d'ensemble des règles de la déduction naturelle} \begin{tabular}{c|c|c} @@ -346,7 +347,7 @@ $\forall$ \\\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}$ +&$\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} @@ -365,6 +366,160 @@ p.ex. $v:I$). \end{frame} % \begin{frame} +\frametitle{Notations des $\lambda$-termes pour $\forall$} + +{\footnotesize + +\itempoint On a vu en calcul propositionnel qu'on peut noter les +démonstrations par des « $\lambda$-termes » qui peuvent ensuite être +réinterprétés comme des programmes (c'est Curry-Howard). Complétons +ces notations pour $\forall, \exists$ : + +\par} + +\medskip + +\itempoint \textcolor{blue}{\underline{Introduction du $\forall$ :}} +si $s$ désigne une preuve de $Q$ faisant intervenir $v$ variable libre +de type $I$, on notera $\lambda(v:I).\,s$ la preuve de +$\forall(v:I).\,Q$ obtenue par introduction du $\forall$. +\[ +\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q} +\] + +\medskip + +\itempoint \textcolor{blue}{\underline{Élimination du $\forall$ :}} si +$f$ désigne une preuve de $\forall(v:I).\,Q$ et $t$ un terme de +type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize + (c'est-à-dire $Q$ avec $v$ remplacé par $t$)} obtenue par +élimination du $\forall$ sur ce terme. +\[ +\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]} +\] + +\medskip + +\itempoint Ceci est conforme à l'idée de BHK : une preuve de +$\forall(v:I).\, Q(v)$ prend un $t$ de type $I$ et renvoie une preuve +de $Q(t)$. + +\end{frame} +% +\begin{frame} +\frametitle{Notations des $\lambda$-termes pour $\exists$} + +\itempoint \textcolor{blue}{\underline{Introduction du $\exists$ :}} +si $t$ désigne un terme de type type $I$ et $z$ une preuve de +$Q[v\backslash t]$ (pour ce $t$-là, donc), on notera $\langle +t,z\rangle$ la preuve de $\exists(v:I).\,Q$ obtenue par introduction +du $\exists$. +\[ +\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q} +\] + +\medskip + +\itempoint \textcolor{blue}{\underline{Élimination du $\exists$ :}} si +$z$ désigne une preuve de $\exists(v:I).\,P$ et $s$ une preuve de $Q$ +faisant intervenir $v$ variable libre de type $I$ et $h$ hypothèse +supposant $P$ (pour ce $v$-là, donc), on notera +$(\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s)$ la +preuve de $Q$ obtenue par élimination du $\exists$. +\[ +\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q} +\] + +\medskip + +\itempoint Ceci est conforme à l'idée de BHK : une preuve de +$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ d'une preuve +de $Q(t)$. + +\end{frame} +% +\begin{frame} +\label{natural-deduction-rules-with-quantifiers-and-notations} +\frametitle{Récapitulatif des notations} + +{\footnotesize(À comparer au + transp. \ref{natural-deduction-rules-with-quantifiers}.)\par} + +\medskip + +\begin{tabular}{c|c|c} +&Intro&Élim\\\hline +$\Rightarrow$ +&\scalebox{0.65}{$\inferrule{\Gamma,v:P\vdash s:Q}{\Gamma\vdash \lambda(v:P).\,s : P\Rightarrow Q}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash f:P\Rightarrow Q\\\Gamma\vdash z:P}{\Gamma\vdash fz:Q}$} +\\\hline +$\land$ +&\scalebox{0.65}{$\inferrule{\Gamma\vdash z_1:Q_1\\\Gamma\vdash z_2:Q_2}{\Gamma\vdash \langle z_1,z_2\rangle : Q_1\land Q_2}$} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_1 z:Q_1}$} +\quad\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_1\land Q_2}{\Gamma\vdash \pi_2 z:Q_2}$} +\\\hline +$\lor$ +&\scalebox{0.65}{$\inferrule{\Gamma\vdash z:Q_i}{\Gamma\vdash \iota_i^{(Q_1,Q_2)}z : Q_1\lor Q_2}$} {\footnotesize ($i\in\{1,2\}$)} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:P_1\lor P_2\\\Gamma,h_1:P_1\vdash s_1:Q\\\Gamma,h_2:P_2\vdash s_2:Q}{\Gamma\vdash (\texttt{match~}r\texttt{~with~}\iota_1 h_1 \mapsto s_1,\; \iota_2 h_2 \mapsto s_2):Q}$} +\\\hline +$\top$ +&\scalebox{0.65}{$\inferrule{\strut}{\Gamma\vdash \bullet:\top}$} +&\scalebox{0.65}{(néant)} +\\\hline +$\bot$ +&\scalebox{0.65}{(néant)} +&\scalebox{0.65}{$\inferrule{\Gamma\vdash r:\bot}{\Gamma\vdash \texttt{exfalso}^{(Q)} r:Q}$} +\\\hline +$\forall$ +&\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$} +&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$} +\\\hline +$\exists$ +&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$} +&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$} +\\ +\end{tabular} + +\end{frame} +% +\begin{frame} +\frametitle{Que peut-on quantifier au juste ?} + +\itempoint Les règles pour les démonstrations écrites notamment +transp. \ref{natural-deduction-rules-with-quantifiers} à \ref{natural-deduction-rules-with-quantifiers-and-notations} +\alert{ne sont pas complètes}, il manque les explications sur les +« individus » : +\begin{itemize} +\item qu'est-ce que c'est que ce « type » $I$ sur lequel on a le droit + de quantifier ? +\item comment forme-t-on des « termes » de type $I$ ? (d'où sortent + ces $\Gamma \vdash t:I$ écrits en gris ?) +\end{itemize} + +\medskip + +\itempoint Différents systèmes logiques diffèrent dans la réponse à +ces questions, notamment, les $8$ systèmes du « $\lambda$-cube » de +Barendregt (certains mélangent complètement preuves et individus). + +\medskip + +\itempoint On ne va décrire plus loin que le cas le plus simple, la +\alert{logique du 1\textsuperscript{er} ordre}, où on ne peut +quantifier que sur \alert{un seul type} très spécial, l'« univers des +individus ». + +\medskip + +\itempoint Évoquons néanmoins auparavant deux problèmes généraux : +\begin{itemize} +\item l'extraction d'informations du $\exists$, +\item l'imprédicativité dans la quantification. +\end{itemize} + +\end{frame} +% +\begin{frame} \frametitle{Le problème du $\exists$ et des types sommes} Doit-on croire à ceci (pour $U$ et $V$ deux types) ? |