pathterminuspages/projects/aboutcontactabout me

Adjoint Between Transition Systems and Hoare Languages

22.08.2020

Contents/Index

Introduction
@Adjoint Between Transition Systems and Hoare Languages
Adjoint Between Transition Systems and Synchronization Trees

Labelled transition system

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:

  1. $\sigma(S_{TS_0}^{I}) = S_{TS_1}^I$, that is $\sigma$ preserves the initial state.
  2. $(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.

Synchronization trees

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) $$

Figure1: A graph of a simple labelled transition system with three states, all accepting.

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),...\}$

Figure2: A graph of a $ST_1$ corresponding to the $TS_1$ in Figure1. The tree is infinite.

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.

Figure3: A graph of $ST_2$ corresponding to $TS_1$ in Figure1. The tree is infinite.

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$.

Figure4 : A graph of $ST_3$ corresponding to $TS_1$ in Figure1, but with a different mapping of labels.

Hoare Languages

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

  1. $\emptyset \neq H_{HL} \subset L_{HL}^{*}$
  2. $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.

The functors HL2ST and ST2HL

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.

Adjoint between HL2ST and ST2HL

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.

Figure4: Diagram of adjoint formed by HL2ST and ST2HL functors.

$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.

Figure5 : The diagram of the natural transformation that arises from $\eta_{ST}$ and $HL2ST \circ ST2HL$.

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.

Embeddings

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: