@Adjoint Between Transition Systems and Hoare Languages

Adjoint Between Transition Systems and Synchronization Trees

A *labelled transition system* is a structure
$$
TS = (S_{TS},s^{I}_{TS},L,Tran_{TS})
$$
where

- $S_{TS}$ is a set of states.
- $s^{I} \in S_{TS}$ is the initial state.
- $L_{TS}$ is a set of labels.
- $Tran_{TS} \subset S_{TS} \times L_{TS} \times S_{TS}$ is the transition relation.

Given two transition systems, $TS_0$ and $TS_1$, an arrow $h : TS_0 \rightarrow TS_1$ is a pair $(\sigma,\lambda)$, where $\sigma : S_{TS_0} \rightarrow S_{TS_1}$ is a function and $\lambda : L_{TS_0} \rightharpoonup L_{TS_1} $ a partial function, such that:

- $\sigma(S_{TS_0}^{I}) = S_{TS_1}^I$, that is $\sigma$ preserves the initial state.
- $(s,a,s') \in Trans_{TS_0}$ implies
- If $\lambda \downarrow a$, then $(\sigma(s),\lambda(a),\sigma(s'))$
- Else $\sigma(s) = \sigma(s')$

Here $f \downarrow x$ means that the partial function $f$ is defined on $x$. We define the category **TS** of labelled transition systems with $TS_0,TS_1, ...$ as objects and the above described as arrows.

A *synchronization tree* is an acyclic, reachable transition system $ST$ such that
$$
(s',a,s),(s'',b,s) \in Trans_{ST} \Rightarrow s' = s'' \land a = b
$$
That is we have no two different incomming paths to any node. We denote this **ST** as a subcategory of **TS**.

Let's develop some intuition behind this. Say we have the $TS$ as in Figure1. Name this $TS_1$. Regarded as a finite automaton where all states are accepting, this transition system defines the same language as the regular expression $$ (ab)^{*}(a|aa|\epsilon) $$

We can translate $TS_1$ into the $ST$ seen in Figure2. Name this $ST_1$. $ST_1$ is infinite in structure (or size) since the language of the corresponding $TS_1$ is infinite.

We have that $L_{ST_1} = \{a,b\}$. We have that $s^{I}_{ST_1} = \{S_0\}$, and we have that $S_{ST_1} = \{S_0, S_1 , ...\}$. And of course that $Tran_{ST_1} = \{(S_0,a,S_1),(S_0,a,S_3),...\}$

The tree in Figure2 is one possible tree. We have an arrow $\eta_{ST} = (\sigma,\lambda)$ in **ST** that translates $ST_1$ into the tree found in Figure3, name this $ST_2$. $\eta_{ST}$ is given as thus
$$
\sigma(s_i) = \{ \alpha | s_0 \xrightarrow{a_0} s_1 \xrightarrow{a_1} \cdots \xrightarrow{a_{i - 1}} s_i \land \alpha = a_0 \cdots a_{i - 1} \}
$$
That is for each state $s_i \in ST_1$ we translate into a path up till $s_i$. So state $s_i$ after translation is named
$$
a_0 \cdots a_{i - 1}
$$
We have that
$$
\lambda = id
$$
since the same set of labels is used.

Note that we do not have an arrow in **ST** from $ST_2$ to $ST_1$. When constructing each new state $s_{\alpha}$, two adjecent paths that comes from the same parrent node and have the same label, are collapsed into one path. We can't use (2) of definition of arrows in **ST** to split the state $s_{\alpha}$ into two states. We call the tree of $ST_2$ the canonical form. Later when we discuss adjunctions, we will return to this canonical form.

The tree as seen in Figure4 can be contructed using $ST_1$ with the same translation used to construct $ST_2$, but with $\lambda$ given as $$ \lambda = [a \mapsto a,b \mapsto c] $$ Name this tree $ST_3$.

A *Hoare language* is a pair $HL = (H_{HL},L_{HL})$ with the two properties

- $\emptyset \neq H_{HL} \subset L_{HL}^{*}$
- $sa \in H_{HL} \Rightarrow s \in H_{HL}$

A partial map $\lambda : HL_0 \rightarrow HL_1$ is a morphism of *Hoare languages* from $(H_{HL_0},L_{HL_0})$ to $(H_{HL_1},L_{HL_1})$ if for each $s \in H_{HL_0}$ we have $\hat{\lambda}(s) \in H_{HL_1}$, where $\hat{\lambda} : L_{HL_0}^{*} \rightarrow L_{HL_1}^{*}$ is given as

- $\hat{\lambda}(\epsilon) = \epsilon$
- $\hat{\lambda}(sa) = \begin{cases} \hat{\lambda}(s)\lambda(a) & \text{if } \lambda \downarrow a \\ \hat{\lambda}(s) & \text{otherwise} \end{cases}$

This gives rise to the category **HL** of *Hoare languages*. With $(H,L)$-tuples as objects and $\lambda$'s as arrows.

Again let's develop some intuition. Say we have $HL_1$. Here we define
$$
L_{HL_1} = \{a,b\}
$$
So we have that $L_{HL_1}^{*}$ is every possible finite combination of series of the symbols $a$ and $b$. We let $H_{HL_1}$ match the language of $TS_1$. That is every possible string we can form with $TS_1$. We have that property *ii* is satisfied, since we can stop in each state in a **TS**, that is we only travel one symbol at a time. So say we are in state $s_i$ of $S_{TS_1}$. This forms the string
$$
\epsilon \cdot a_0 \cdot a_1 \cdots a_i \in H_{HL_1}
$$
Note that if we stop at state $s_0$, we have the string $\epsilon$. Now we can just take one step back to $s_{i - 1} \in S_{TS_{1}}$, from where we can construct the string
$$
\epsilon \cdot a_0 \cdot a_1 \cdots a_{i - 1} \in H_{HL_1}
$$
We can do this recursively until the string $\epsilon$ is reached. This corresponds to how we have defined $\sigma$ in arrows of **ST**: the parent of state $s_i$ is named
$$
\epsilon \cdot a_0 \cdots a_{i - 2}
$$

We create $HL_2$ in the exact same manner, but with $$ L_{HL_2} = \{a,c\} $$ There's an arrow between $HL_1$ and $HL_2$. That is $\lambda_{HL}$ for which $$ \lambda_{HL} = [a \mapsto a,b \mapsto c] $$ Substituting symbols is exactly what $\lambda$ recursively does.

We need the following two functors in order to construct an adjoint. First we construct $ST2HL : ST \rightarrow HL$ in the following manner. For objects we treat the tree in the same way as the $\sigma$ part of arrows for **ST**, but used repeatedly on every state of the tree. That is we translate as
$$
ST2HL(ST_1) = (\{ \alpha | s_1 \xrightarrow{a_1} \cdots \xrightarrow{a_{i - 1}} s_i \land \alpha = a_1 \cdots a_{i - 1} \},L_{ST_1})
$$
As stated earlier: A Hoare Language corresponds to a $ST$ where state $s_i$ is named
$$
\epsilon \cdot a_0 \cdots a_{i - 1}
$$
With this setup the arrow between $ST_1$ and $ST_2$ is collapsed into the arrow between $HL_1$ and $HL_1$, that is the $id$ arrow. This holds in general, since we in **HL** only have the canonical version of any $ST$.

Second we construct $HL2ST : HL \rightarrow ST$ in the following manner: $$ HL2ST((H_{HL_1},L_{HL_1})) = (H_{HL_1},\epsilon,L_{HL_1},\{ (\alpha,a,\alpha a) | \alpha , \alpha a \in H_{HL_1} \}) $$ Again: we name the states of the resulting $ST$ with strings from $H_{HL}$. We name the initial state $\epsilon$. We use the alphabet $L_{LH}$ as labels. And we create a transition on symbol $a$ from $s_i$ to $s_{i + 1}$ if and only if $s_{i + 1}$ is named $s_i \cdot a$.

Due to that an $ST$ only have one representation in **HL**, we have that
$$
HL2ST(ST2HL(ST_1)) = ST_2
$$
The behavior of $ST2HL \circ HL2ST$ is the same as for arrows in **ST**, we rename the states using the concatenation of strings up till a given state.

We can construct an adjoint from the above functors. First note as stated above that
$$
ST_2 = HL2ST(ST2HL(ST_1)) = \eta_{ST}(ST_1)
$$
Furthermore let $h$ be the arrow in **ST** between $ST_1$ and $ST_3$. And note that there is an arrow $\lambda_{HL}$ between $HL_1$ and $HL_2$. This arrow is the same as the arrow between $ST2HL(ST_1)$ and $HL_2$. And it is exactly the arrow that makes the diagram of Figure4 commute.

$ST2HL$ is the left adjoint. And $HL2ST$ the right.

The arrow $\eta_{ST_{1}}$ is given as
$$
\eta_{ST_{1}} : id(ST_1) \rightarrow HL2ST(ST2HL(ST_{1}))
$$
where
$$id : \textbf{ST} \rightarrow \textbf{ST}$$
is the identity functor. Thus we conform to the definition of an adjoint. $\eta_{ST}$ is a natural transformation and hence a family of functions. That is for every **ST**-arrow $h'$ the diagram in Figure5 commutes.

We of course have an arrow between $HL_1$ and $HL_1$, the identity arrow. So we also have an arrow between $ST2HL(ST_1)$ and $HL_1$.

In general for $ST_i$ we have that $HL2ST(ST2HL(ST_i)) = ST^{can}_{i}$, where $ST^{can}_{i}$ is the canonical form of $ST_{i}$. For each arrow
$$
h : ST_i \rightarrow HL2ST(HL_j) = ST^{can}_i
$$
there is exactly one arrow
$$
\lambda_{HL} : ST2HL(ST_i) \rightarrow HL_j
$$
since objects in **HL** are canonical forms of objects in **ST**.

We say that **HL** is embedded in **ST** since every $HL \in \textbf{HL}$ can be mapped into a $ST \in \textbf{ST}$. Though this map is not surjective, eg. $ST_1$ can't be the target of $HL2ST$. However the functor $ST2HL$ is surjective. So **ST** contains **HL** in terms of $HL2ST$, but **ST** is bigger in size than **HL**.

CommentsGuest Name:Comment: