add predicate transformer

Start section on fibrational framework for nested alternating fixed points.
Show how the predicate transformer is built in the univariate case and how it is extended to the multivariate case.

beamer/beamer.tex

@@ -35,6 +35,15 @@
 \DeclareMathOperator{\new}{new}
 \DeclareMathOperator{\sym}{sym}
 
+\setbeamertemplate{section page}
+{
+    \begin{centering}
+    \begin{beamercolorbox}[sep=12pt,center]{part title}
+    \usebeamerfont{section title}\insertsection\par
+    \end{beamercolorbox}
+    \end{centering}
+  }
+  
 % ChkTex parameters
 % chktex-file 3
 % chktex-file 18
@@ -219,7 +228,121 @@
 % Rel :  - objets relations X^2 -> \Omega
 %%%%%%%% - flèches fonction k : X -> Y tq P \sqsubseteq Q \circ (k \times k)
 %%%%%%%% - k^*Q = Q \circ (k \times k)
-% Espaces métriques
-% Espaces topologiques
+% Espaces métriques, espaces topologiques : structure additionnelle sur la catégorie de base
+% opérateur fibrationnel -> composé d'opérations communes à toutes les fibrations
 % on peut généraliser un concept à d'autres fibrations en changeant le relèvement cartésien
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section*{Cadre fibrationnel pour points fixes imbriqués}
+
+\begin{frame}
+  \sectionpage
+\end{frame}
+
+% après étude bibliographique, première partie du stage -> étendre le lien entre théorie des jeux et + grand point fixe de l'opérateur fibrationnel
+% alterner entre élément de ces travaux et l'extension que j'en ai faite -> montre la façon dont j'ai procédé
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Transformateur de prédicats \tiny [Komorida+, LICS'19]}
+  \begin{figure}[t]
+    \centering
+    \begin{tikzpicture}[every circle/.style={x radius = .5, y radius = 1}]
+      \uncover<2->{
+        \node (C) at (0,2) {$\mathbb{C}$} ;
+        \node (B) at (0,0) {$\mathbb{B}$} ;
+        \path [->] (C) edge node[left] {$p$} (B) ;
+      }
+      \uncover<3->{
+        \node (X) at (2,0) {$X$} ;
+        \node (FX) at (4,0) {$FX$} ;
+        \path [->] (X) edge node[below] {$c$} (FX) ;
+        \draw[dashed] (2,2) circle ;
+        \draw[dashed] (4,2) circle ;
+      }
+      \uncover<4->{
+        \node (Omega) at (8,0) {$\Omega$} ;
+        \draw[dashed] (8,2) circle ;
+        \node (OMEGA) at (8,1.5) {$\boldsymbol{\Omega}$} ;
+      }
+      \uncover<5->{
+        \node (FOmega) at (6,0) {$F\Omega$} ;
+        \path [->] (FOmega) edge node[below] {$\tau$} (Omega) ;
+        \draw[dashed] (6,2) circle ;
+      }
+      \uncover<6->{
+        \node (P) at (2,2.5) {$P$} ;
+        \path [->] (P) edge node[above] {$f$} (OMEGA) ;
+        \path [->,dashed] (FX) edge node[below] {$F(pf)$} (FOmega) ;
+        \path [->] (X) edge[bend right] node[below] {$pf$} (Omega) ;
+      }
+      \uncover<7->{
+        \node (*OMEGA) at (2,1.5) {$k^*\boldsymbol{\Omega}$} ;
+        \path [->] (*OMEGA) edge node[below] {$\overline{c}$} (4,1.5)
+        (4,1.5) edge node[below] {$\overline{F(pf)}$} (6,1.5)
+        (6,1.5) edge node[below] {$\overline{\tau}$} (OMEGA) ;
+      }
+    \end{tikzpicture}
+  \end{figure}
+  \uncover<8->{
+    \[ \Phi_c^{\boldsymbol{\Omega},\tau}P = \bigsqcap_{f : P \rightarrow \Omega} (\tau \circ F(pf) \circ c)^*\boldsymbol{\Omega} \]
+  }
+\end{frame}
+
+% d'abord opérateur fibrationnel = transformateur de prédicats
+% données : - fibration
+%%%%%%%%%%% - système de transitions
+%%%%%%%%%%% - objet témoin (pour fibration de prédicats ou relation \Omega treillis complet)
+%%%%%%%%%%% - fonction d'évaluation
+% si P dans le fibré de X et f : P -> OMEGA : projette f, applique F, obtient FX -> F\Omega
+% flèche complète : on la tire en arrière
+% faire ça pour toutes les flèches : on obtient transformateur de prédicats
+% intuition : plus grand objets tel que pour tout f, \tau \circ Fpf \circ c conserve la structure donnée par la fibration
+% par exemple on peut obtenir bisimulation comme plus grand point fixe
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Transformateur de prédicats à plusieurs variables}
+  \begin{figure}[t]
+    \centering
+    \begin{tikzpicture}[every circle/.style={x radius = .5, y radius = 1}]
+      \uncover<2->{
+        \node (C) at (0,2) {$\mathbb{C}$} ;
+        \node (B) at (0,0) {$\mathbb{B}$} ;
+        \path [->] (C) edge node[left] {$p$} (B) ;
+        \node (X) at (2,0) {$X$} ;
+        \node (FX) at (4,0) {$FX$} ;
+        \path [->] (X) edge node[below] {$c$} (FX) ;
+        \draw[dashed] (2,2) circle ;
+        \draw[dashed] (4,2) circle ;
+        \node (Omega) at (9,0) {$\Omega$} ;
+        \draw[dashed] (9,2) circle ;
+        \node (OMEGA) at (9,1.5) {$\boldsymbol{\Omega}$} ;
+        \only<2>{\node (FOmega) at (7,0) {$F\Omega$} ;}
+        \path [->] (FOmega) edge node[below] {$\tau$} (Omega) ;
+        \draw[dashed] (7,2) circle ;
+      }
+      \uncover<3->{
+        \node (FOmega) at (7,0) {$F(\Omega^{\textcolor{purple}{2}})$} ;
+      }
+      \uncover<4->{
+        \node (P) at (2,2.5) {$\textcolor{purple}{P_1,P_2}$} ;
+        \path [->] (P) edge node[above] {$\textcolor{purple}{f_1,f_2}$} (OMEGA) ;
+        \path [->,dashed] (FX) edge node[below] {$F\textcolor{purple}{\langle pf_1,pf_2 \rangle}$} (FOmega) ;
+        \path [->] (X) edge[bend right] node[below] {$pf_1,pf_2$} (Omega) ;
+      }
+      \uncover<5->{
+        \node (*OMEGA) at (2,1.5) {$k^*\boldsymbol{\Omega}$} ;
+        \path [->] (*OMEGA) edge (OMEGA) ;
+      }
+    \end{tikzpicture}
+  \end{figure}
+  \uncover<6->{
+    \[ \Phi_c^{\boldsymbol{\Omega},\tau} (\textcolor{purple}{\seq{P}{n}}) = \bigsqcap_{\textcolor{purple}{\substack{f_1 : P_1 \rightarrow \Omega \\ \ldots \\ f_n : P_n \rightarrow \Omega}}} (\tau \circ F\textcolor{purple}{\langle\seq{pf}{n}\rangle} \circ c)^*\boldsymbol{\Omega} \]
+  }
+\end{frame}
+
+% passage de plus grand point fixe à points fixes imbriqués => nécessite fonction à plusieurs variables
 \end{document}