Interleaving Models

@The adjoint pair of functors HL2ST and ST2HL

The adjoint pair of functors ST2TS and TS2ST

The goal of this section is to create an adjoint pair of functors between the categories $\textbf{ST}$ and $\textbf{HL}$. In order to create the adjoint we need functors between the two categories. The resulting functors reveals how the two categories are related in terms of how one is embedded in the other.

We need the following two functors. First we construct $ST2HL : \textbf{ST} \rightarrow \textbf{HL}$ in the following manner. For objects we treat the tree in the same way as how $\sigma$ treats states for $\textbf{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 in 2.3.1: 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 itself, the $id$ arrow. This holds in general, since we in $\textbf{HL}$ only have the canonical version of any $ST$ - as the basic example in the introduction shows.

Second we construct $HL2ST : \textbf{HL} \rightarrow \textbf{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} \}) $$ This is the same as how we treat arrows in $\textbf{ST}$: 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 some $ST$ only have the canonical representation in $\textbf{HL}$, we have that $$ HL2ST(ST2HL(ST_1)) = ST_2 $$ The behavior of $ST2HL \circ HL2ST$ is the same as for arrows in $\textbf{ST}$, we rename the states using the concatenation of strings up till a given state.

We can construct an adjunction 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 \CatST 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 Figure 6 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 $\textbf{ST}$-arrow $h'$ the diagram in Figure 7 commute.

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 $\textbf{HL}$ are canonical forms of objects in $\textbf{ST}$.

Let $\textbf{HL}(HL_1,HL_2)$ denote the class of arrows in $\textbf{HL}$ from object $HL_1$ to object $HL_2$. Denote in the same manner for classes of arrows in $\textbf{ST}$. We have that the map
$$
HL2ST : \textbf{HL}(HL_1,HL_2) \rightarrow \textbf{ST}(HL2ST(HL_1),HL2ST(HL_2))
$$
is surjective. That is every arrow in $\textbf{ST}(HL2ST(HL_1),HL2ST(HL_2))$ is constructed by $HL2ST$ on some arrow in $\textbf{HL}(HL_1,HL_2)$. In regards of this property we say that $HL2ST$ is *full*. We have that this map is also injective. That is every arrow of $\textbf{ST}(HL2ST(HL_1),HL2ST(HL_2))$ is constructed with $HL2ST$ by some unique arrow in $\textbf{HL}(HL_1,HL_2)$. In regards of this property we say that $HL2ST$ is *faithful*. We have that $HL2ST$ is injective on objects. So in total we say that $HL2ST$ is an embedding.

However $ST2HL(ST_1 \rightarrow ST_2) = ST2HL(id_{ST_1})$, hence we do not have an embedding the other way. So $\textbf{ST}$ contains $\textbf{HL}$ in terms of $HL2ST$, but $\textbf{ST}$ is bigger in size than $\textbf{HL}$. Thus the $ST2HL$ functor abstracts away branching structure, or conversely we see $\textbf{HL}$ as a more abstract version of $\textbf{ST}$.

CommentsGuest Name:Comment: