diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 43 |
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 |