Functoriality of connectors and of logical formulae.

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