From ba3e964176370407d8f187ca8833f27e7acdaf8c Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 14:36:50 +0100
Subject: Positive and negative occurrences.

---
 transp-inf110-02-typage.tex | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

(limited to 'transp-inf110-02-typage.tex')

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
@@ -2490,6 +2490,49 @@ B\Rightarrow C)$ est une tautologie, donc
 en est une (par substitution de $D\Rightarrow E$ pour $A$, de
 $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:
-- 
cgit v1.2.3