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

diag added but needs more work!

Browse Source
This commit is contained in:
partowp
2026-09-22 20:30:18 +01:00
parent d8ff38f5b2
commit fc57a27811
1 changed files with 39 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+39 -6
View File
@@ -106,6 +106,7 @@
\usepackage{xspace} \usepackage{xspace}
\usepackage{bm} \usepackage{bm}
\usepackage{pifont} \usepackage{pifont}
\usepackage{circuitikz}
\input{catprog} \input{catprog}
@@ -1558,21 +1559,31 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
\begin{tikzpicture}[ \begin{tikzpicture}[
scale=0.5, every node/.style={transform shape} scale=0.6, every node/.style={transform shape}
] ]
\matrix (m) [matrix of nodes, \matrix (m) [matrix of nodes,
nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
align=center, font=\scriptsize, inner sep=2pt}, align=center, font=\scriptsize, inner sep=2pt},
row sep=6mm, column sep=6mm] row sep=6mm, column sep=6mm]
{ {
$\appr\cdot-$-Hughes-Jacobs & $\appr\cdot-$-Hermida-Jacobs & $\appr\cdot-$-Span-based & $\appr\cdot-$-Aczel-Mendler \\ AM-simulation & left-lax simulation\\
$-\cdot\appr$-Hughes-Jacobs & $-\cdot\appr$-Hermida-Jacobs & $-\cdot\appr$-Span-based & $-\cdot\appr$-Aczel-Mendler \\ & bi-lax simulation & mid-lax simulation \\
$\appr\cdot-\cdot\appr$-Hughes-Jacobs & $\appr\cdot-\cdot\appr$-Hermida-Jacobs & $\appr\cdot-\cdot\appr$-Span-based & $\appr\cdot-\cdot\appr$-Aczel-Mendler \\ HJ-simulation & left-lax simulation\\
}; };
% Example arrows (uncomment / edit as needed): % 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-1) to[bend right=30] node[midway, above] {AC} (m-1-1);
\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] (m-3-1); \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1);
\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above] {liftable} (m-2-3);
\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2);
\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, above] {coliftable} (m-2-3);
\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2);
\draw[-{Latex[length=2mm]}] (m-1-2) to node {liftable $\&$ coliftable} (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2);
\draw[-{Latex[length=2mm]}] (m-3-2) to node {liftable $\&$ coliftable} (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1);
\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
\end{tikzpicture} \end{tikzpicture}
@@ -1646,6 +1657,28 @@ Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{
The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators. The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.
\end{rem} \end{rem}
Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it! Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it!
%\begin{equation}
% \begin{figure}[!ht]
% \centering
% \resizebox{1\textwidth}{!}{%
% \begin{circuitikz}
% \tikzstyle{every node}=[font=\fontsize{14.2pt}{18.5pt}\selectfont]
% \draw (3,12.5) ellipse (2.125cm and 0.625cm);
% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (3,12.5) {AM-simulation};
% \draw (8.625,13.125) ellipse (2.25cm and 0.625cm);
% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (8.625,13.125) {HJ-simulation};
% \draw (1.5,10.375) ellipse (1.875cm and 0.625cm);
% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (1.5,10.375) {F-simulation};
% \draw (6.75,10.625) ellipse (2.75cm and 0.625cm);
% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (6.75,10.625) {F\comp\appr-simulation};
% \draw (9.625,8) ellipse (2.625cm and 0.625cm);
% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (9.5,8) {\appr\comp F-simulation};
% \end{circuitikz}
% }%
% \caption{Your Caption}
% \label{fig:my_label}
% \end{figure}
%\end{equation}
%\begin{figure}[t] %\begin{figure}[t]
% \centering % \centering
% \begin{tabular}{|l|c|c|} % \begin{tabular}{|l|c|c|}