pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

pc sync

Browse Source
This commit is contained in:
Sergey Goncharov
2026-09-11 15:33:23 +01:00
parent dde56ad7d8
commit 83b4910d0e
1 changed files with 44 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+44 -4
View File
@@ -82,6 +82,8 @@
\usetikzlibrary{arrows.meta}
\usetikzlibrary{decorations} % Required for all decorations
\usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag'
\usetikzlibrary{matrix,positioning,arrows.meta,shapes.geometric}
\tikzset{
commutative diagrams/.cd,
@@ -1403,6 +1405,44 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
\end{proof}
%
\subsection{Simulations in Set}
%\begin{figure}[ht]
% \centering
% \begin{tabular}{|c|c|c|c|c|}
% \hline
% & \textbf{Hughes-Jacobs} & \textbf{Hermida-Jacobs} & \textbf{Span-based} & \textbf{Aczel-Mendler} \\
% \hline
% $\appr\cdot-$ & ? & ? & ? & ? \\
% \hline
% $-\cdot\appr$ & ? & ? & ? & ? \\
% \hline
% $\appr\cdot-\cdot\appr$ & ? & ? & ? & ? \\
% \hline
% \end{tabular}
% \caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.}
% \label{fig:anonymous_onymous_transposed}
%\end{figure}
\begin{tikzpicture}[
scale=0.5, every node/.style={transform shape}
]
\matrix (m) [matrix of nodes,
nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
align=center, font=\scriptsize, inner sep=2pt},
row sep=6mm, column sep=6mm]
{
$\appr\cdot-$-Hughes-Jacobs & $\appr\cdot-$-Hermida-Jacobs & $\appr\cdot-$-Span-based & $\appr\cdot-$-Aczel-Mendler \\
$-\cdot\appr$-Hughes-Jacobs & $-\cdot\appr$-Hermida-Jacobs & $-\cdot\appr$-Span-based & $-\cdot\appr$-Aczel-Mendler \\
$\appr\cdot-\cdot\appr$-Hughes-Jacobs & $\appr\cdot-\cdot\appr$-Hermida-Jacobs & $\appr\cdot-\cdot\appr$-Span-based & $\appr\cdot-\cdot\appr$-Aczel-Mendler \\
};
% Example arrows (uncomment / edit as needed):
\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, above] {AC} (m-3-2);
\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] (m-3-1);
\end{tikzpicture}
Traditionally, simulations in $\Set$ are defined using relators. In this section we make a comparison on this concept with the other notions of simulation that we mentioned.
%\begin{notation}
% We show the category of sets and binary relations with $\rels$, and we show a morphism in this category as $R\c X\rto Y$ that is a relation $R$.
@@ -1417,7 +1457,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
%\end{proof}
%The above translation seems to be true in a more general case, where $\spa$ and $\rel$ are defined on an arbitrary category (the latter is called an allegory then).
\begin{definition}[Relator]\label{def:relator}
Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\Rel$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$.
Assuming $F$ is a functor on $\Set$, an $F$-relator or simply a relator $\relar$ is a monotone map that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\Rel$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$.
\end{definition}
%
%\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim-rela}
@@ -1458,10 +1498,10 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
\end{example}
%
\begin{prop}\label{prop:HeJ-HuJ}
For a functor $F\c\Set\to\Set$, every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$:
Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$,
\begin{enumerate}
\item is a $\tilde{F}$-simulation if it is a Hermida-Jacobs simulation.
\item is a Hermida-Jacobs simulation if it is a $\tilde{F}$-simulation, assuming the axiom of choice.
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.
\end{enumerate}
\end{prop}
\begin{proof}