diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 147 |
1 files changed, 123 insertions, 24 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index b16d9a6..c0aeb08 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2487,56 +2487,155 @@ B\Rightarrow C)$ est une tautologie, donc \[ ((D\Rightarrow E)\land (E\Rightarrow D) \Rightarrow D) \Rightarrow ((D\Rightarrow E)\Rightarrow (E\Rightarrow D)\Rightarrow D) \] -en est une (par substitution de $D\Rightarrow E$ pour $A$, de -$E\Rightarrow D$ pour $B$, et de $D$ pour $C$). +en est (par subst\textsuperscript{ion} de $D\Rightarrow E$ pour $A$, +de $E\Rightarrow D$ pour $B$, et de $D$ pour $C$). + +\medskip + +{\footnotesize + +\itempoint Attention, ce polymorphisme s'applique aux +\alert{conclusions, pas aux hypothèses} (l'hypothèse $A$ ne permet pas +de tout déduire !). + +\par} \end{frame} % \begin{frame} -\frametitle{Occurrences positives et négatives} +\frametitle{« Fonctorialité » des connecteurs logiques} -\itempoint Dans une formule propositionnelle / type dont \alert{toutes - les variables sont distinctes} (on parle alors d'« occurrences »), -on va définir des occurrences \textcolor{purple}{\textbf{positives}} -(=\textcolor{purple}{croissantes}, \textcolor{purple}{covariantes}) et -\textcolor{olive}{\textbf{négatives}} -(=\textcolor{olive}{décroissantes}, -\textcolor{olive}{contravariantes}) par induction : \begin{itemize} -\item une variable propositionnelle seule est une occurrence positive, -\item dans $Q_1\land Q_2$ ainsi que $Q_1\lor Q_2$, toutes les - occurrences positives (resp. négatives) dans $Q_1$ et $Q_2$ le sont - dans la formule tout entière, -\item dans $P\Rightarrow Q$, les occurrences positives - (resp. négatives) dans $Q$ le sont dans la formule mais les - occurrences dans $P$ sont inversées. +\item Donnés $t_1 : \tau_1 \to \tau_1'$ et $t_2 : \tau_2 \to \tau_2'$, + le terme $\lambda (u : \tau_1\times\tau_2).\langle t_1(\pi_1 u), + t_2(\pi_2 u)\rangle$ est de type $\tau_1\times\tau_2 \to + \tau_1'\times\tau_2'$. +\item Donnés $t_1 : \tau_1 \to \tau_1'$ et $t_2 : \tau_2 \to \tau_2'$, + le terme $\lambda (u : + \tau_1+\tau_2). (\texttt{match~}u\texttt{~with~}\iota_1 v_1 \mapsto + \iota_1^{(\tau_1',\tau_2')} (t_1v_1),\; \iota_2 v_2 \mapsto + \iota_2^{(\tau_1',\tau_2')} (t_2v_2))$\\est de type $\tau_1+\tau_2 \to + \tau_1'+\tau_2'$. +\item Donnés $s : \sigma' \to \sigma$ (\textcolor{olive}{attention au + sens !}) et $t : \tau \to \tau'$, le terme $\lambda (u : + \sigma\to\tau). \lambda (x:\sigma'). t(u(sx))$ est de type + $(\sigma\to\tau) \to (\sigma'\to\tau')$. \end{itemize} -\medskip +\bigskip -\itempoint Occurrences \textbf{strictement positives} : ce sont les -variables seules, et les s-positives de $Q_1,Q_2,Q$ dans $Q_1\land -Q_2$, $Q_1\lor Q_2$ et $P\Rightarrow Q$. +Donc, par Curry-Howard : + +\begin{itemize} +\item Si $Q_1\Rightarrow Q_1'$ et $Q_2\Rightarrow Q_2'$ alors + $(Q_1\land Q_2)\Rightarrow (Q_1'\land Q_2')$. +\item Si $Q_1\Rightarrow Q_1'$ et $Q_2\Rightarrow Q_2'$ alors + $(Q_1\lor Q_2)\Rightarrow (Q_1'\lor Q_2')$. +\item Si $P'\Rightarrow P$ (\textcolor{olive}{attention au sens !}) et + $Q\Rightarrow Q'$ alors $(P\Rightarrow Q)\Rightarrow (P'\Rightarrow + Q')$. +\end{itemize} \bigskip {\footnotesize -P.ex. dans +\itempoint On dit que $\land$ et $\lor$ sont +\textcolor{purple}{\textbf{croissants}} (ou +\textcolor{purple}{covariants}) en leurs deux arguments, et que +$\Rightarrow$ l'est dans son argument de droite, mais qu'il est +\textcolor{olive}{\textbf{décroissant}} (ou +\textcolor{olive}{contravariant}) dans son argument de gauche. + +\par} + +\end{frame} +% +\begin{frame} +\frametitle{Sous-formules positives et négatives} + +Dans une formule propositionnelle, on définit les sous-formules +\textcolor{purple}{\textbf{positives}} (voire \textbf{strictement + positives}) et \textcolor{olive}{\textbf{négatives}} par induction : +\begin{itemize} +\item les sous-formules \textcolor{purple}{positives} de $Q_1\land Q_2$ et $Q_1\lor Q_2$ + sont la formule tout entière, et les sous-formules \textcolor{purple}{positives} de + $Q_1$ et celles de $Q_2$, +\item les sous-formules \textcolor{olive}{négatives} de $Q_1\land Q_2$ et $Q_1\lor Q_2$ + sont les sous-formules \textcolor{olive}{négatives} de $Q_1$ et celles de $Q_2$, +\item les sous-formules \textcolor{purple}{positives} de $P \Rightarrow Q$ sont la formule + tout entière, les sous-formules \textcolor{purple}{positives} de $Q$ et les + \emph{\textcolor{olive}{négatives}} de $P$, +\item les sous-formules \textcolor{olive}{négatives} de $P \Rightarrow + Q$ sont les sous-formules \textcolor{olive}{négatives} de $Q$ et les + \emph{\textcolor{purple}{positives}} de $P$. +\end{itemize} + +\smallskip + +{\footnotesize + +\itempoint Les sous-formules strict\textsuperscript{t} positives de +$Q_1\land Q_2$ et $Q_1\lor Q_2$, resp. $P\Rightarrow Q$ sont la +formule tout entière et les sous-formules strict\textsuperscript{t} +positives de $Q_1$ et de $Q_2$ (resp. $Q$). + +\par} + +\medskip + +{\footnotesize + +P.ex. dans\vskip-5ex \[ ({\color{olive}A}\Rightarrow ({\color{olive}B}\Rightarrow {\color{purple}C})) \land (({\color{purple}D}\Rightarrow {\color{olive}E})\Rightarrow {\color{purple}F}) \] les occurrences ${\color{purple}C},{\color{purple}D},{\color{purple}F}$ sont positives -($D$ et $F$ strictement), tandis que +($C$ et $F$ strictement), tandis que ${\color{olive}A},{\color{olive}B},{\color{olive}E}$ sont négatives. \par} \end{frame} % +\begin{frame} +\frametitle{« Fonctorialité » des formules} + +Conséquence de la fonctorialité des connecteurs logiques : + +\smallskip + +\itempoint Si $S$ est une formule propositionnelle et $S'$ obtenue en +remplaçant une sous-formule positive $Q$ par $Q'$ telle que $Q +\Rightarrow Q'$, alors $S \Rightarrow S'$. + +\smallskip + +\itempoint Si $S$ est une formule propositionnelle et $S'$ obtenue en +remplaçant une sous-formule négative $P$ par $P'$ telle que $P' +\Rightarrow P$, alors $S \Rightarrow S'$. + +\bigskip + +Comme toute sous-formule est soit positive soit négative, on en +déduit : + +\smallskip + +\itempoint Corollaire : Si $S$ est une formule propositionnelle et +$S'$ obtenue en remplaçant une sous-formule quelcone $R$ par $R'$ +telle que $R \Leftrightarrow R'$, alors $S \Leftrightarrow S'$. + +\medskip + +P.ex., on peut remplacer $Q_1\land Q_2$ par $Q_2\land Q_1$ ou +$(Q_1\land Q_2)\land Q_3$ par $Q_1\land (Q_2\land Q_3)$ n'importe où +dans une formule et on obtient ainsi une formule équivalente. + +\end{frame} +% % TODO: -% - substitution d'équivalences % - présentation en calcul des séquents % - élimination des coupures % - Kripke |