Commit 96422487 authored by Quentin Aristote's avatar Quentin Aristote
Browse files

make more compact

parent eab69fe7
......@@ -13,6 +13,7 @@
\usepackage{enumitem}
\usepackage[sorting=none]{biblatex}
\addbibresource{biblio.bib}
% \renewcommand*{\bibfont}{\small}
\newtheorem{definition}{Definition}[subsection]
\newtheorem{corollary}[definition]{Corollary}
......@@ -970,7 +971,7 @@ The concept of codensity bisimilarity is expressive enough to instantiate the cl
Codensity bisimilarities can be characterized by the winning positions of the following game. In particular, since codensity bisimilarities are greatest fixed points, this game is a safety game.
\begin{definition}[untrimmed codensity safety game]
\begin{definition}[untrimmed codensity safety game]\label{def:untrimmed-codensity-safety-game}
The \emph{untrimmed codensity safety game} (originally the untrimmed codensity game for bisimilarity) is the safety game shown in Table~\ref{tab:untrimmed-codensity-safety-game}.
\begin{table*}[h]
\centering
......@@ -1037,19 +1038,19 @@ Although the previous theorem gives the expected categorical link between bisimu
We then get a smaller game, still characterizing codensity bisimilarities, that is reminescent of the classic bisimulation game~\cite{stirlingBisimulationModalLogic1999} and instantiates a new game characterizing the bisimulation distance.
\begin{definition}[trimmed codensity safety game]
Let $\mathcal{G}$ be a generating set of the fiber $\mathbb{C}_X$. The \emph{trimmed codensity safety game} is the safety game shown in Table~\ref{tab:trimmed-codensity-safety-game}.
\begin{table*}[h]
\centering
\begin{tabular}{c c c}
Position & Player & Possible moves \\
\toprule
$P \in \mathcal{G}$ & S & \makecell{$\sigma \in \Sigma$, $k : X \rightarrow \Omega_\sigma$ such that \\ $P \not\sqsubseteq (\tau_\sigma \circ Fk \circ c)^*\mathbf{\Omega}_\sigma$} \\
\midrule
$k : X \rightarrow \Omega_\sigma$ & D & $P \in \mathcal{G}$ such that $P \not\sqsubseteq k^*\mathbf{\Omega}_\sigma$ \\
\bottomrule
\end{tabular}
\caption{Trimmed codensity safety game}\label{tab:trimmed-codensity-safety-game}
\end{table*}
Let $\mathcal{G}$ be a generating set of the fiber $\mathbb{C}_X$. The \emph{trimmed codensity safety game} is the same game as the (untrimmed) codensity safety game (Definition~\ref{def:untrimmed-codensity-safety-game}), except D can only play moves in $\mathcal{G}$ (instead of $\mathbb{C}_X$). % safety game shown in Table~\ref{tab:trimmed-codensity-safety-game}.
% \begin{table*}[h]
% \centering
% \begin{tabular}{c c c}
% Position & Player & Possible moves \\
% \toprule
% $P \in \mathcal{G}$ & S & \makecell{$\sigma \in \Sigma$, $k : X \rightarrow \Omega_\sigma$ such that \\ $P \not\sqsubseteq (\tau_\sigma \circ Fk \circ c)^*\mathbf{\Omega}_\sigma$} \\
% \midrule
% $k : X \rightarrow \Omega_\sigma$ & D & $P \in \mathcal{G}$ such that $P \not\sqsubseteq k^*\mathbf{\Omega}_\sigma$ \\
% \bottomrule
% \end{tabular}
% \caption{Trimmed codensity safety game}\label{tab:trimmed-codensity-safety-game}
% \end{table*}
\end{definition}
\begin{theorem}\label{theorem:invariants-joint-codensity-bisimulations}
......@@ -1092,10 +1093,7 @@ Since the Henessy-Milner theorem gives a deep relationship between bisimulations
&= \tau \circ F(\ellipsis{f}{1}{\times}{n})
\end{align*}
since $k \mapsto \tau \circ Fk$ is monotone. Therefore if $(\id_X,\ldots,\id_X) : X \rightarrow X^n$,
\begin{align*}
F^{\id_\Omega,\tau}(\seq{f}{n}) \circ F(\id_X,\ldots,\id_X) &= \tau \circ F(\seq{f}{n}) \\
&= \sem{\tau}(\seq{f}{n})
\end{align*}
\[ F^{\id_\Omega,\tau}(\seq{f}{n}) \circ F(\id_X,\ldots,\id_X) = \sem{\tau}(\seq{f}{n})\]
\end{example}
Assume the setting of Definition~\ref{def:multivariate-codensity-lifting}, and let $c : X \rightarrow FX$ be an $F$-coalgebra.
......@@ -1563,20 +1561,19 @@ For completeness, Theorem~\ref{theorem:transfer-codensity-bisimilarity} was also
\begin{theorem}[Transfer of codensity equational systems]\label{theorem:transfer-codensity-equational-systems}
Let $q : \mathbb{D} \rightarrow \mathbb{B}$ be another \clatfibration{} and let $T : \mathbb{C} \rightarrow \mathbb{D}$ be a full fibered functor from $p$ to $q$ preserving both fibered meets and joins.
\[
\begin{tikzcd}
\mathbb{C} \arrow[rr,"T"] \arrow[dr, "p"] & & \mathbb{D} \arrow[dl, "q"] \\
& \mathbb{B} \arrow[loop, out=300, in=240, looseness = 6, "F"] &
\end{tikzcd}
\]
% \[
% \begin{tikzcd}
% \mathbb{C} \arrow[rr,"T"] \arrow[dr, "p"] & & \mathbb{D} \arrow[dl, "q"] \\
% & \mathbb{B} \arrow[loop, out=300, in=240, looseness = 6, "F"] &
% \end{tikzcd}
% \]
For all $i \in [1,m]$, $(T\mathbf{\Omega}_i = (T\mathbf{\Omega}_{i,\sigma})_{\sigma \in \Sigma},\tau_i)$ parameterizes an $n$-variable codensity lifting along $q$~: write $\left(\widetilde{l}_i^{\mathrm{sol}}\right)_{i \in [1,m]}$ for the solution of the following codensity equational system.
\begin{align*}
u_1 =_{\eta_1} &\Phi_{c_1}^{T\mathbf{\Omega}_1,\tau_1}\left(\seq{u}{m}\right) \\
&\vdots \\
u_m =_{\eta_m} &\Phi_{c_m}^{T\mathbf{\Omega}_m,\tau_m}\left(\seq{u}{m}\right)
\end{align*}
Recall that $\left(l_i^\mathrm{sol}\right)_{i \in [1,m]}$ stands for the solutions of $E$ (Equational System~\eqref{eq:codensity-equational-system}). Then, for all $i \in [1,m]$,
\[ T\left(l_i^\mathrm{sol}\right) = \widetilde{l}_i^{\mathrm{sol}} \]
Recall that $\left(l_i^\mathrm{sol}\right)_{i \in [1,m]}$ stands for the solutions of $E$ (Equational System~\eqref{eq:codensity-equational-system}). Then, for all $i \in [1,m]$, $T\left(l_i^\mathrm{sol}\right) = \widetilde{l}_i^{\mathrm{sol}}$.
\end{theorem}
% % \begin{proof}
......@@ -1847,7 +1844,7 @@ holds if and only if $\Phi_c^{{\Leftrightarrow},\exists}\left(r\right)(x,y) = 1$
(b,\place) & \mapsto & b
\end{array} \right.
\]
and choose $\mathbf{\Omega}_{i,j} = (\mathbf{\Omega}_{i,j,\sigma})_{\sigma \in \Sigma \cup \{\epsilon\}}$ for all $i,j \in 2$ with $\mathbf{\Omega}_{i,j,\sigma} : \Omega^2 \rightarrow \Omega$ depending only on $\sigma$ for $\sigma \in \Sigma$ (we write $\mathbf{\Omega}_\sigma$) and
and choose $\mathbf{\Omega}_{i,j} = (\mathbf{\Omega}_{i,j,\sigma})_{\sigma \in \Sigma \cup \{\epsilon\}}$ for all $i,j \in 2$ with $\mathbf{\Omega}_{i,j,\sigma} : \Omega^2 \rightarrow \Omega$ depending only on $\sigma \in \Sigma$ (we write $\mathbf{\Omega}_\sigma$) and
\[
\mathbf{\Omega}_{i,j,\epsilon} : \left\{
\begin{array}[h]{c c c}
......@@ -2070,7 +2067,7 @@ They are also instances of a class of equational systems for which more specific
(b,\place) & \mapsto & b
\end{array} \right.
\]
and choose $\mathbf{\Omega}_{p,q} = (\mathbf{\Omega}_{p,q,\sigma})_{\sigma \in \Sigma \cup \{\epsilon\}}$ for all $p,q \in 2$ with $\mathbf{\Omega}_{p,q,\sigma} : \Omega^2 \rightarrow \Omega$ depending only on $\sigma$ (we write $\mathbf{\Omega}_\sigma$) for $\sigma \in \Sigma$ and
and choose $\mathbf{\Omega}_{p,q} = (\mathbf{\Omega}_{p,q,\sigma})_{\sigma \in \Sigma \cup \{\epsilon\}}$ for all $p,q \in 2$ with $\mathbf{\Omega}_{p,q,\sigma} : \Omega^2 \rightarrow \Omega$ depending only on $\sigma \in \Sigma$ (we write $\mathbf{\Omega}_\sigma$) and
\[
\mathbf{\Omega}_{p,q,\epsilon} : \left\{
\begin{array}[h]{c c c}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment