Positive and negative occurrences.

1 files changed, 43 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 131e3f2..b16d9a6 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2492,6 +2492,49 @@ $E\Rightarrow D$ pour $B$, et de $D$ pour $C$).
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Occurrences positives et négatives}
+
+\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.
+\end{itemize}
+
+\medskip
+
+\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$.
+
+\bigskip
+
+{\footnotesize
+
+P.ex. dans
+\[
+({\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
+${\color{olive}A},{\color{olive}B},{\color{olive}E}$ sont négatives.
+
+\par}
+
+\end{frame}
+%
 % TODO:
 % - substitution d'équivalences
 % - présentation en calcul des séquents