1 Introduction↩︎

It is a well-known secret that relational semantics (e.g.Kripke semantics) arises from dualities, i.e.categorical equivalences of the form \(F : \Op{\CC} \Equiv \DD\). The idea is that \(\CC\) is a ‘spatial’ category whose objects are frames, and \(\DD\) is an ‘algebraic’ category whose objects are algebras of predicates, which allow reasoning about the elements of the frames.

For example, truth table semantics for infinitary classical propositional logic arises from the Tarski duality \(\Op{\SET} \Equiv \CABA\) between the category of sets and the category of complete atomic Boolean algebras (CABAs) [1].¹ The Kripke semantics of infinitary classical modal logic [3], [4] arises from the Thomason duality \(\Op{\FRMOPEN} \Equiv \CABAO\) between the category of Kripke frames and the category of CABAs with operators (i.e.modalities) [5] [1, Sec. 2.4]. The Kripke semantics of infinitary intuitionistic logic [6] arises from the duality \(\Op{\POSET} \Equiv \PRIMEALGLATT\) between posets and prime algebraic lattices [7], [8]. Famous dualities of this form include Stone duality (for Boolean algebras) [9], Jónsson-Tarski duality [10]–[12] (for Boolean algebras with operators), and Esakia duality [13] (for Heyting algebras). See the chapter by Kishida [1] for further references.

The overwhelming majority of work in this area has not paid much attention to the logical rôle of morphisms of these categories.² In many cases the ‘frame’ morphisms \(f : W \to W'\) of \(\CC\) can be thought of as ‘truth-preserving’: they map worlds to worlds in a way that preserves and reflects truth, i.e.\(w \vDash \varphi\) iff \(f(w) \vDash \varphi\). The corresponding morphism \(\Pre{f} : F(W') \to F(W)\) of \(\DD\) then preserves the logical structure, e.g.\(\Pre{f}(\varphi \land \psi) = \Pre{f}(\varphi) \land \Pre{f}(\psi)\). Thus \(\Pre{f}\) can be considered as mapping predicates over \(W'\) to predicates over \(W\), in a manner that preserves logical connectives.

Obtaining this property in the case of intuitionistic and modal logics requires strong properties on frame morphisms. For example, in the Kripke semantics of modal logic the induced map \(\Pre{f} : \Powerset*{W'} \to \Powerset*{W}\) preserves the modality \(\Box\) iff \(f : W \to W'\) is an open map, i.e.a transition-preserving function whose graph is a (functional) bisimulation [1].³

However, functionality is incidental to the idea of bisimulation. It is natural to wonder what happens if we relax the morphisms of \(\CC\), requiring them to merely be relations instead of functions. Answering this question would allow us to have categories \(\CC\) consisting of frames and well-behaved relations, e.g.bisimulations. A duality of this form would then put bisimulations in correspondence with a different kind of morphism between algebras, enabling reasoning ‘across’ a bisimulation.

Such results, which may be called relational dualities, can already be found in the literature. However, most of them put relations between frames in correspondence with hemimorphisms, i.e.morphisms that preserve most—but not all!—logical connectives. For example, a relation \(R \subseteq W \times W'\) uniquely corresponds to a function \(W \to \Powerset*{W'}\), which uniquely corresponds to a function \(\Pre{R} : \Powerset*{W'} \to \Powerset*{W}\) that preserves all joins (but not necessarily all meets) [10] [1, Sec. 2.3].

This is unsatisfactory from a computational perspective. Traditional dualities allow us to compute the ‘action’ of a morphism of frames \(f : W \to W'\) on the syntax of a formula. Given a formula \(\varphi\) (over \(W'\)) we can define a formula \(\Pre{f}(\varphi)\) (over \(W\)) by recursion. For example, in Tarski duality this would be computed by defining \(\Pre{f}(\varphi \land \psi) \defeq \Pre{f}(\varphi) \land \Pre{f}(\psi)\) and so on. Thus, \(\Pre{f}\) can be pushed through all connectives until it reaches a propositional variable \(p\), where it returns a predicate \(f^{-1}(p)\) which is true at \(w\) exactly when \(p\) is true at \(f(w)\). Hence, a function \(f : W \to W'\) allows us to map predicates on \(W'\) to predicates on \(W\) in a logic-preserving manner. As hemimorphisms do not preserve all logical connectives, it is impossible to adapt this definition to a relation \(R \subseteq W \times W'\).

To tackle this difficulty this paper develops a different type of duality, viz. one that puts relations \(R \subseteq W \times W'\) between frames in correspondence with relations \(\mathcal{F}(R) \subseteq F(W) \times F(W')\) between predicates. This allows us to view \(\mathcal{F}(R)\) as a relational judgment between formulae pertaining to different systems, with \(R\) playing the rôle of a ‘background theory’ which specifies how propositions over the two systems are related. The ultimate goal is to develop a formal system for synthetically reasoning about the relation between formulae over different frames. It is not difficult to imagine that this might have applications in program logics.

If the relation \(R \subseteq W \times W'\) is also a bisimulation between frames, it can be thought of as a notion of equivalence between the states of two systems, with \(w \Rel{R} w'\) meaning that \(w\) and \(w'\) have the same behaviours. Viewed as a judgment, the induced relation \(\mathcal{F}(R) \subseteq F(W) \times F(W')\) then satisfies ‘inference rules,’ which we wish to identify.

As we are interested in bisimulations, we take a hint from the relevant literature on coalgebra [17]–[19] and base all the results in this paper on the lower lifting, which maps a relation \(R \subseteq W \times W'\) to the lower relation \(\Lower{R} \subseteq \Powerset*{W} \times \Powerset*{W'}\), defined by \[S \Lower{R} T\;\defequiv\;\forall s \in S.\;\exists t \in T.\;s \Rel{R} t.\] Famously, this construction is not a functor \(\REL \fto \REL\), as it does not preserve identities. However, we can define an appropriate category \(\CABAREL\) with CABAs as objects, so that it becomes a functor \(\Lower : \REL \fto \CABAREL\). Surprisingly, this functor is an equivalence. Moreover, \(\Lower\) ‘extends’ Tarski duality, in the sense that the diagram \[\begin{tikzcd} \Op{\SET} \ar[r, hook] \ar[d, "\Equiv" left] & \Op{\REL} \ar[d, "\Equiv" left, "\Lower \circ (-)^\dagger" right] \\ \CABA \ar[r, hook] & \CABAREL \end{tikzcd}\] commutes, where \({(-)}^\dagger : \Op{\REL} \cong \REL\) is the obvious formal duality that reverses a relation. This follows a known pattern wherein relational dualities are not really ‘dualities’ per se, but become so only after composition with a formal duality [1] [20] Remark 4.1. In this light the \(\Op{(-)}\) is merely an artifact of functionality.

After recalling some definitions to fix notation (2), we briefly recap the elements of the Tarski duality \(\Op{\SET} \Equiv \CABA\) (3). Then, we show that the lower lifting given above can be used to extend it to a relational Tarski duality (4). We achieve this by precisely characterising the relations between CABAs that are obtained as lower liftings, and hence establish an equivalence. Furthermore, we show that this is an extension of the usual Tarski duality, and sketch the formal system that this duality induces.

Following this, we show how the same lifting gives rise to a relational version of the Thomason duality \(\Op{\FRMOPEN} \Equiv \CABAO\) (5). This is somewhat more challenging: while the Tarski duality acts on arbitrary functions, the Thomason duality associates open maps (i.e.functional bisimulations) with modal complete Boolean homomorphisms. We show that this has an analogue on the relational level, putting (bi)simulations in unique correspondence with what we call (bi)simulatory relations between CABAs. We show that this relational Thomason duality extends the duality originally given by Thomason, and again sketch the formal system that this duality induces. We close with a discussion of related work (6).

2 Preliminaries↩︎

A relation \(R : A \relto B\) from a set \(A\) to a set \(B\) is a subset \(R \subseteq A \times B\). We write \(a \Rel{R} b\) to mean \((a, b) \in R\). If \(R : A \relto B\) and \(S : B \relto C\) their composition \(R \then S : A \relto C\) is defined in the usual manner, i.e.\(a \Rel*{R \then S} c\) just if there exists some \(b \in B\) with \(a \Rel{R} b \Rel{S} c\). Note that we write the composition of relations using diagrammatic order. Given a relation \(R : A \relto B\) we define its opposite \(\Rev{R} : B \relto A\) by \(b \Rel{\Rev{R}} a\) iff \(a \Rel{R} b\). Sets and relations form a category \(\REL\) under composition, with the identity \(\Id_A : A \relto A\) given by \(a_1 \Rel{\Id_A} a_2\) iff \(a_1 = a_2\). Moreover, the opposite construction extends to a functor \(\Rev{(-)} : \Op{\REL} \to \REL\) which constitutes a formal duality \(\Op{\REL} \cong \REL\) given by taking the opposite. This shows that \(\REL\) is a dagger category, i.e.equipped with an involutive contravariant functor [21, Sec. 2.3.1].

A partial order \((P, \sqsubseteq_P)\) is a set \(P\) equipped with a relation \(\mathord{\sqsubseteq_P} : P \relto P\) which is reflexive, transitive, and anti-symmetric. We will commonly refer to partial orders by their carriers (\(P\), \(Q\), …) and often elide the subscript of \(\sqsubseteq\). A function \(f : P \to Q\) is monotonic just if \(x \sqsubseteq_P y\) implies \(f(x) \sqsubseteq_Q f(y)\). A lattice is a partial order that has all finite joins and meets. We will use \(\mathcal{L}, \mathcal{L}', \ldots\) to denote lattices. A complete lattice \(\mathcal{L}\) is a partial order that has all joins, which also implies that it has all meets. A pair of monotonic functions \(f : P \to Q\) and \(g : Q \to P\) is an adjunction (which in this setting is also called a Galois connection) just if \(f(x) \sqsubseteq_Q y\) iff \(x \sqsubseteq_P g(y)\). This is often denoted by \(f \adjoint g\). It is a consequence that \(f\) preserves any joins that exist in \(P\) and \(g\) preserves any meets that exist in \(Q\). The adjoint functor theorem [22, Sec. 7.34] [9] says that if \(f : P \to Q\) is monotonic, \(P\) is a complete lattice, and \(f\) preserves all joins, then \(f\) has a right adjoint \(g : Q \to P\). Dually, if \(g : Q \to P\) is monotonic, \(Q\) is a complete lattice, and \(g\) preserves all meets, then \(g\) has a left adjoint \(f : P \to Q\). We refer the reader to the book by Davey and Priestley [22] for background on orders, and to the books by Mac Lane, Awodey, and Riehl [23]–[25] for category theory.

3 A Primer on Tarski Duality↩︎

We recap the Tarski duality \(\Op{\SET} \Equiv \CABA\), and show how it induces an infinitary classical propositional logic. Recall that a Boolean algebra is a distributive lattice \(\mathcal{B}\) in which every element \(x \in \mathcal{B}\) has a complement \(\lnot x \in \mathcal{B}\) for which \(x \lor \lnot x = \top\) and \(x \land \lnot x = \bot\) [9].

For any set \(X\), its powerset \(\Powerset*{X}\) is a Boolean algebra [22, Sec. 5.2]. In fact, it is a complete Boolean algebra, i.e.a complete lattice with joins and meets of \((S_i)_{i \in I}\) given by \(\bigcup_{i \in I} S_i\) and \(\bigcap_{i \in I} S_i\) respectively. Moreover, \(\Powerset*{X}\) is atomic, in the following sense.

A complete atomic Boolean algebra (CABA) is then a complete Boolean algebra \(\mathcal{B}\) which is moreover atomic. For any set \(X\), the powerset \(\Powerset*{X}\) is a CABA: its atoms are exactly the singleton sets \(\{ x \}\) for \(x \in X\): every \(S \subseteq X\) can be reconstructed as \(S = \bigcup_{x \in S} \{ x \}\).

A morphism of CABAs \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) is a monotonic function that preserves all meets and joins. This definition has some significant implications. First, as \(\mathcal{B}\) and \(\mathcal{B}'\) are Boolean algebras, every such \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) is a complete Boolean homomorphism, i.e.preserves all Boolean connectives, including negation. Second, by the adjoint functor theorem the map \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) has both a left and a right adjoint: \[\begin{tikzcd}[column sep=huge] \mathcal{B}' \arrow[r, bend left=40, "f_!"] \arrow[r, bend right=40, "f_*"'] & \mathcal{B} \arrow[l, "f^*" description] \arrow[phantom, from=1-1, to=1-2, "{\rotatebox[origin=c]{-90}{\dashv}}" pos=0.5, shift left=3.5, description] \arrow[phantom, from=1-1, to=1-2, "{\rotatebox[origin=c]{-90}{\dashv}}", pos=0.5, shift right=3.5, description] \end{tikzcd}\] CABAs and their morphisms form a category \(\CABA\).

Given any function \(f : X \to Y\) we can define a complete Boolean homomorphism \(\Pre{f} : \Powerset*{Y} \to \Powerset*{X}\) by \(\Pre{f}(B) = \SetComp{ x \in X }{ f(x) \in B}\) [1], [26], [27]. By the adjoint functor theorem, \(\Pre{f}\) has both a left and a right adjoint, respectively given by \[\begin{align} {2} \LKan{f}(A) &= \SetComp{ y \in Y }{\exists x \in X.\;f(x) = y \land x \in A } &&= \SetComp{ f(x) }{ x \in A } \\ \RKan{f}(A) &= \SetComp{ y \in Y }{ \forall x \in X.\;f(x) = y \Rightarrow x \in A } &&= \SetComp { y \in Y }{ \Pre{f}(\{ y \}) \subseteq A }. \end{align}\] Thus, we obtain a functor \(\Powerset : \Op{\SET} \fto \CABA\).

In order to invert this functor we use some properties of its adjoints. The following lemma is standard: it follows from the facts that atoms and primes coincide in CABAs, and that the left adjoint of a complete lattice homomorphism preserves primes [28].

We can thus define a functor \(\At : \CABA \to \Op{\SET}\), which maps a CABA \(\mathcal{B}\) to its set of atoms \(\At{\mathcal{B}}\), and use 1 to map a morphism \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) to the restriction \(\LKan{f}|_{\At{\mathcal{B}'}} : \At{\mathcal{B}'} \to \At{\mathcal{B}}\) of its left adjoint to atoms.

This is a pseudo-inverse to \(\Powerset\), and we obtain a categorical equivalence.

The gist is that every CABA \(\mathcal{B}\) is isomorphic to the powerset \(\Powerset*{\At{\mathcal{B}}}\) of its atoms: its elements are uniquely determined by the atoms below them.

This duality induces (infinitary) classical propositional logic. Let \(W\) be a set of worlds. This set corresponds to the powerset \(\Powerset*{W}\), which can be seen as a set of predicates. A world \(w \in W\) satisfies the predicate \(\varphi \in \Powerset*{W}\) just if \(w \in \varphi\). As \(\Powerset*{W}\) is a Boolean algebra, predicates are closed under all Boolean operations.⁴ Individual worlds \(w \in W\) correspond to singleton predicates \(\{ w \} \in \Powerset*{W}\) which uniquely characterise them. If we interpret \(W\) as the set of states of a computer, logics of this ilk have been in continuous employment since the pioneering work of Dijkstra [29].

4 A Relational Tarski Duality↩︎

If instead of a function \(f : W \to W'\) we were to have an arbitrary relation \(R : W \relto W'\), what would the corresponding morphism between \(\Powerset*{W}\) and \(\Powerset*{W'}\) be?

It is possible to obtain such a duality by enlarging \(\CABA\) to \(\CABAJoin\), whose morphisms only preserve joins, and then show that \(\REL \Equiv \CABAJoin\) [10], [30] [1]. Indeed, if \(h : \Powerset*{X} \to \Powerset*{Y}\) preserves all joins, then—by writing any set as a union of singletons—we see that \(h\) is completely determined by a function \(X \to \Powerset*{Y}\), i.e.a relation \(X \relto Y\). Hofmann and Nora [31] show that this duality is a special case of a general one. However, these more general morphisms do not preserve the logical structure of predicates. For example it may be that \(h(\varphi \land \psi) \neq h(\varphi) \land h(\psi)\). We have thereby lost the benefit of being able to recursively compute \(h\) on the syntax of formulae.

Instead, we would like a duality whose logical side consists of predicates and relations. To construct one we consider a simple way of lifting relations to powersets [32].

This lifting has a long history. It is one half of the Egli-Milner lifting, which first appeared in the powerdomain literature [33], [34]. It then resurfaced in the coalgebra literature [17], where post-fixed-points amount to simulations between transition systems [19]. Intuitively, \(S \Lower{R} T\) means every state of \(S\) can be ‘\(R\)-simulated’ by a state of \(T\).

\(\Lower\) maps a relation between sets to a relation between CABAs. However, it is not a functor \(\REL \fto \REL\), as it maps the identity relation \(\id : X \relto X\) to the containment relation \(\mathbin{\subseteq} : \Powerset*{X} \relto \Powerset*{X}\). We will define a category \(\CABAREL\) so that \(\Lower\) becomes a functor \(\REL \fto \CABAREL\). The relations between CABAs will be characterised as follows.

It is simple to show that directionally atomic relations compose, and that \(\sqsubseteq\) is the identity.

We can therefore define a category \(\CABAREL\) with CABAs as objects, and directionally atomic relations as morphisms. We can then construct a functor:

One can identify a pseudo-inverse for \(\Lower\), viz.the functor \(\At : \CABAREL \fto \REL\) which restricts every relation \(R : \mathcal{L} \relto \mathcal{L}'\) to atoms: \[\begin{align} \At{\mathcal{L}} &\defeq \SetComp{x \in \mathcal{L}}{x \text{ is an atom of } \mathcal{L}}, & \Rel{\At{R}} &\defeq \Rel{R}|_{\At{\mathcal{L}} \times \At{\mathcal{L}'}}. \end{align}\] This is a functor: when \(a\) and \(c\) are atoms, any witness for \(a \Relcomp{R \then S} c\) can be replaced by an atomic witness using atomic-foundedness of \(R\) and bimodularity of \(S\).

Of course, 2 is not explicitly a duality; to make it one we have to compose it with the formal duality \(\Rev{(-)} : \Op{\REL} \Equiv \REL\) in the style of Kishida [1], obtaining

Intuitively, the fact that \(\REL\) is a dagger category means that its morphisms have no inherent direction. Directionality appears when we restrict it to functions, making this equivalence a ‘proper’ duality [1, Sec. 2.3] [20]. Indeed, it is possible to show that this duality is an extension of the usual Tarski duality, in the sense that there is a commutative diagram \[\label{diagram:reltarski-extends-tarski} \begin{tikzcd} \Op{\SET} \ar[r, hook, "\Op{\Graph}"] \ar[d, "\Powerset" left, "\Equiv" right] & \Op{\REL} \ar[d, "\Equiv" left, "\Lower \circ (-)^\dagger" right] \\ \CABA \ar[r, hook, swap, "j"] & \CABAREL \end{tikzcd}\tag{1}\] where \(\Graph\) and \(j\) are faithful and injective-on-objects.

We define \(j\) by taking each CABA \(\mathcal{B}\) to itself, and each complete Boolean homomorphism \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) to \(j(\Pre{f}) : \mathcal{B} \relto \mathcal{B}'\) given by \(b \Rel{j(\Pre{f})} b'\) just if \(b \sqsubseteq \LKan{f}(b')\), where \(\LKan{f} \Adjoint \Pre{f}\).

We define \(\Graph\) by taking each set \(X\) to itself, and each function \(f : X \to Y\) to its graph \(\Graph{f} : X \relto Y\), viz. \(x \Graph{f} y \defequiv (f(x) = y)\).

Finally, 1 commutes: for \(f : X \to Y\), both routes send \(f\), seen as a morphism \(Y \to X\) in \(\Op{\SET}\), to the relation \(A \subseteq \LKan{f}(B)\) between \(A \in \Powerset*{Y}\) and \(B \in \Powerset*{X}\).

4.1 Sketch of a Formal System↩︎

Having developed this duality we can now see how it can be used for relating formulae. Suppose we have a relation \(R : X \relto Y\). Under the relational Tarski duality this induces a relation \(\Lower{R} : \Powerset*{X} \relto \Powerset*{Y}\) between predicates. We denote this relation by the judgment \[\Simulates{\varphi}{R}{\psi}\] where \(\varphi \in \Powerset*{X}\) is a predicate over \(X\) and \(\psi \in \Powerset*{Y}\) over \(Y\). Intuitively, this judgment says that every state of \(X\) that satisfies \(\varphi\) is \(R\)-related to some state of \(Y\) that satisfies \(\psi\). The fact \(\Lower{R}\) is a bimodule means that the rule

is sound. This is reminiscent of the consequence rule of Hoare logic [35].

The fact \(\Lower{R}\) is left-disjunctive means that the rule

is sound. This allows us to reason by cases on the left. The final characteristic property of \(\Lower{R}\), namely its atomic-foundedness, would require introducing judgments that capture atomicity of predicates, in the style of Abramsky [14].

Finally, the fact \(\Lower\) is a functor can be formally expressed by the rules

5 A Modal Relational Duality↩︎

In this section we will extend the relational Tarski duality to (infinitary) classical modal logic. The basis for this is the Thomason duality [5] [1], which uniquely associates each Kripke frame with a CABA equipped with a modal operator (CABAO).

A Kripke frame \((X, R)\) (also called a transition system) is a set \(X\) equipped with a relation \(R : X \relto X\). The intuition is that \(X\) is a set of worlds, and the relation \(R\) encodes transitions from one world to another. We will sometimes write \(x_1 \Transition{R} x_2\) instead of \(x_1 \Rel{R} x_2\). A morphism of Kripke frames \(f : (X, R) \to (Y, S)\) is a function \(f : X \to Y\) which preserves transitions, meaning \(x_1 \Transition{R} x_2\) implies \(f(x_1) \Transition{S} f(x_2)\). Kripke frames and their morphisms form a category \(\FRM\).

The relation \(R\) can also be seen as a map \(\lambda R : X \to \Powerset*{X}\) by currying. Then there is a unique join-preserving function \(\blacklozenge_R : \Powerset*{X} \to \Powerset*{X}\) that makes the following diagram commute, where \(\Yo : X \to \Powerset*{X}\) maps every element \(x \in X\) to the singleton set \(\{ x \}\).⁵ \[\begin{tikzcd}[column sep=huge,row sep=large] X \ar[r, "\Yo"] \ar[dr,"\lambda R" below left] & \Powerset*{X} \ar[d,dashed,bend right=40,"\blacklozenge_R" left,""{name=diamond,right}] \\ & \Powerset*{X} \ar[u,dotted,bend right=40,"\Box_R" right,""{name=square,left}] \ar[phantom, from=diamond, to=square, "\Adjoint"] \end{tikzcd}\] As \(\blacklozenge_R\) preserves joins and \(\Powerset*{X}\) is a complete lattice, the adjoint functor theorem implies that it has a right adjoint \(\Box_R : \Powerset*{X} \to \Powerset*{X}\), which preserves all meets.

These maps are explicitly given by \[\begin{align} \blacklozenge_R(A) &= \SetComp{w \in X}{\exists v \in A.\;v \Rel{R} w}, & \Box_R(A) &= \SetComp{w \in X}{\forall v \in X.\;w \Rel{R} v \implies v \in A}. \end{align}\] Having one of these three pieces of data (the relation \(R\); a join-preserving map \(\blacklozenge_R\); or a meet-preserving map \(\Box_R\)) uniquely determines the other two [8].

It is possible to define morphisms of frames purely in terms of operators:

Let \(\CABAOW\) be the category whose objects \((\mathcal{B}, \Box_\mathcal{B})\) are CABAs \(\mathcal{B}\) equipped with an operator \(\Box_{\mathcal{B}} : \mathcal{B} \to \mathcal{B}\) that preserves all meets,⁶ and morphisms \(\Pre{f} : (\mathcal{B}, \Box_\mathcal{B}) \to (\mathcal{B}', \Box_{\mathcal{B}'})\) are complete Boolean homomorphisms \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) that satisfy \(\Pre{f} \circ \Box_\mathcal{B} \sqsubseteq \Box_{\mathcal{B}'} \circ \Pre{f}\) (with the pointwise order). This yields a modal duality

The maps of CABAOs preserve the Boolean structure, but they only preserve \(\Box\) weakly. To strengthen this we need the notion of an open map.

We let \(\FRMOPEN\) be the wide subcategory of \(\FRM\) whose morphisms are open. It is easy to show that such an \(f\) is open iff \(f^* \circ \Box = \Box \circ f^*\). Then, letting \(\CABAO\) be the wide subcategory of \(\CABAOW\) whose morphisms \(\Pre{f}\) preserve \(\Box\) (i.e.\(\Pre{f} \circ \Box = \Box \circ \Pre{f}\)) we obtain a refinement of 4:

To obtain a relational version of this duality we must relax the functionality of morphisms of Kripke frames. To achieve that, notice that the notion of an open map is precisely a functional bisimulation [36, Sec. 3.2]. Hence, we replace open maps with general (bi)simulations.

We illustrate the definitions of simulation and cosimulation pictorially: \[\begin{tikzcd} x' \ar[r,dashed,"Q"] & {\exists y'} \\ x \ar[u,"R"] \ar[r,"Q"] & y \ar[u,dotted,"S"] \end{tikzcd} \quad\quad\quad \begin{tikzcd} {\exists x'} \ar[r,dashed,"Q"] & y' \\ x \ar[u,dotted,"R"] \ar[r,"Q"] & y \ar[u,"S"] \end{tikzcd}\] These two conditions are often called the forth and the back conditions respectively.

It is easy to see that an open map is exactly a function whose graph is a bisimulation. Indeed, the fact it preserves transitions means it is a simulation (i.e.it satisfies the ‘forth’ condition). The fact it is open means it is a cosimulation (i.e.it satisfies the ‘back’ condition).

(Co)simulations are closed under relational composition, and the identity relation is a bisimulation. We thus obtain two categories \(\FRMSIM\) and \(\FRMBISIM\) with Kripke frames as objects, and simulations and bisimulations as morphisms respectively. Note that the opposite of a simulation is a cosimulation, and vice versa. Therefore, there is a formal duality \(\Rev{(-)} : \Op{\FRMBISIM} \Equiv \FRMBISIM\), meaning \(\FRMBISIM\) is also a dagger category.

It is possible to characterise simulations purely in terms of the lower relation.

Define \(\CABAOSIM\) to have CABAs with operators \((\mathcal{B}, \Box_\mathcal{B})\) as objects and simulatory relations \(Q : (\mathcal{B}, \Box_\mathcal{B}) \relto (\mathcal{B}', \Box_{\mathcal{B}'})\) as morphisms. We will often write these morphisms simply as \(Q : \mathcal{B} \relto \mathcal{B}'\) and omit subscripts. Using the preceding proposition, this is a category, with \(\sqsubseteq\) as an identity morphism.

We can define a functor \(\At : \CABAOSIM \fto \FRMSIM\) by restricting a simulatory relation to atoms, as before. Using [lemma:simulatory] it is easy to check that \(\At{R}\) is a simulation.

In summary, we obtain an equivalence

As in our previous relational duality, the directionality disappears in the relational case. We could turn this result into a duality by composing it with a formal duality between \(\FRMSIM\) and the category of cosimulations. However, this is somewhat awkward.

Our final objective is to restrict this equivalence by analogy to the restriction of \(\Op\FRM \Equiv \CABAOW\) to \(\Op\FRMOPEN \Equiv \CABAO\), where the maps in \(\Op\FRMOPEN\) are open, and correspondingly the maps in \(\CABAO\) preserve all logical connectives. In our relational duality the morphisms are no longer functional, but merely simulations. Thus, openness will turn them into bisimulations.

Unfortunately, expressing bisimulations using our current vocabulary is not immediately possible. For that we will need the following ‘dual’ relational lifting.

It is easy to see that \(\Upper{R} = \Lower{R^\dagger}^\dagger\) for any \(R : X \relto Y\). This makes the theory dual, in the sense that \(\Upper{R}\) is opdirectionally atomic (i.e.right-disjunctive, atomic op-founded, and an opbimodule). To avoid this proliferation of concepts we will simply work with the opposite relation \(\Lower{\Rev{R}}\). We can construct this relation directly on relations between CABAs.

This acts in the expected way between lifted relations.

As every directionally atomic relation is in the image of \(\Lower\), 15 implies that the variant of a directionally atomic relation is directionally atomic. Hence, the variant construction forms a functor \(\Variant{(-)} : \Op{\CABAREL} \fto \CABAREL\) which sends every CABA to itself, and every directionally atomic relation to its variant. Moreover,

Thus, we have a self-duality on \(\CABAREL\), which makes the following claims straightforward.

As with simulations and 10, it is possible to characterise cosimulations purely in terms of the variant relation.

The following proposition is analogous to [proposition:simulatory-compose].

Call a relation bisimulatory if it is both simulatory and cosimulatory. Let \(\CABAOBISIM\) be the category whose objects are CABAOs and whose morphisms are bisimulatory relations. As before, \(\sqsubseteq\) is the identity.

The next four lemmas are the bisimulation analogues of [lemma:lower-frmsim-functor,lemma:lower-frmsim-faithful,lemma:lower-frmsim-full,lemma:lower-frmsim-dense].

We thus obtain the following equivalence.

As before, this is not explicitly a duality, but we can obtain one from the formal duality \((-)^\dagger : \Op{\FRMBISIM} \Equiv \FRMBISIM\).

We can show that 9 is an extension of the Thomason duality; as with 1 , there is a commutative diagram of functors \[\label{diagram:relthomason-extends-thomason-open} \begin{tikzcd} \Op{\FRMOPEN} \ar[r,hook,"\Op{\Graph}"] \ar[d,"\Powerset" left, "\Equiv" right] & \Op{\FRMBISIM} \ar[d,"\Lower \circ (-)^\dagger" right, "\Equiv" left] \\ \CABAO \ar[r,hook,swap,"j"] & \CABAOBISIM \end{tikzcd}\tag{2}\] where \(\Graph\) and \(j\) are faithful and injective-on-objects.

We define \(j\) as before, by taking each CABAO \((\mathcal{B}, \Box_{\mathcal{B}})\) to itself, and each complete Boolean homomorphism \(\Pre{f} : \mathcal{B} \to \mathcal{B}'\) to \(j(\Pre{f}) : \mathcal{B} \relto \mathcal{B}'\) given by \(b \Rel{j(\Pre{f})} b'\) iff \(b \sqsubseteq f_!(b')\).

As usual, \(\Graph\) takes each frame \((X, R)\) to itself and each open map \(f : (X, R) \to (Y, S)\) to the graph \(\Graph{f} : X \relto Y\) defined by \(x \Graph{f} y\) iff \(f(x) = y\).

Finally, a direct calculation shows that 2 commutes.

5.1 Sketch of a Formal System↩︎

Recall the formal system of the judgment \(\Simulates{}{Q}{}\) for a relation \(Q : X \relto Y\) that we sketched in 4. Now assume that \((X, R)\) and \((Y, S)\) are Kripke frames. We can extend this system to a modal logic where the logics over \(X\) and \(Y\) have corresponding modalities \(\blacklozenge\) and \(\Box\). If \(Q\) is a simulation then by [lemma:sim-black,lemma:simulatory] we can extend the system with the rules

If \(Q\) is a cosimulation, then by [lemma:cosim-black,lemma:cosimulatory,lemma:variant-lower] we obtain the rules

which could also be obtained just by noting \(\Rev{Q}\) is a simulation.

5.2 A Worked Example: Bisimulation Between Buffer Systems↩︎

We will now show how to use these rules to reason over a particular bisimulation. The two frames both model a buffer holding a single natural number. However, the two buffers have internal branching: the first has two different ‘ways’ of holding a number (the left and right slots), while the second one has three (slots A, B, and C). This might happen if the buffer is provided by a distributed cluster of machines whose internal structure is not observable.

Define \((X, \to_X)\) by letting \(X = \Set{\textsf{empty}_X} \cup \SetComp{\textsf{L}(n), \textsf{R}(n)}{n \in \mathbb{N}}\) with \[\textsf{empty}_X \to_X \textsf{L}(n) \qquad \textsf{empty}_X \to_X \textsf{R}(n) \qquad \textsf{L}(n) \to_X \textsf{empty}_X \qquad \textsf{R}(n) \to_X \textsf{empty}_X\] for all \(n \in \mathbb{N}\). Similarly, define \((Y, \to_Y)\) by \(Y = \Set{\textsf{empty}_Y} \cup \SetComp{\textsf{A}(n), \textsf{B}(n), \textsf{C}(n)}{n \in \mathbb{N}}\) with \[\textsf{empty}_Y \to_Y \textsf{A}(n) \qquad \textsf{empty}_Y \to_Y \textsf{B}(n) \qquad \textsf{empty}_Y \to_Y \textsf{C}(n)\] \[\textsf{A}(n) \to_Y \textsf{empty}_Y \qquad \textsf{B}(n) \to_Y \textsf{empty}_Y \qquad \textsf{C}(n) \to_Y \textsf{empty}_Y\] for all \(n \in \mathbb{N}\). There is a bisimulation \(Q : X \relto Y\) between these frames given by \[Q = \Set{(\textsf{empty}_X, \textsf{empty}_Y)} \cup \SetComp{(w, v)}{n \in \mathbb{N},\;w \in F_X(n),\;v \in F_Y(n)}\] where \(F_X(n) = \Set{\textsf{L}(n), \textsf{R}(n)}\) and \(F_Y(n) = \Set{\textsf{A}(n), \textsf{B}(n), \textsf{C}(n)}\). In other words, full states holding the same value are related, and so are empty states. This is evidently a non-functional bisimulation.

We define the following predicates, parametrised by \(n \in \mathbb{N}\). On \(X\) let \(\mathit{empty}_X = \Set{\textsf{empty}_X}\), \(L_n = \Set{\textsf{L}(n)}\), and \(R_n = \Set{\textsf{R}(n)}\). On \(Y\) let \(\mathit{empty}_Y = \Set{\textsf{empty}_Y}\).

We will use the following facts as the ‘background theory’: \[\begin{align} \blacklozenge\, \mathit{empty}_X &= \textstyle\bigvee_{n} F_X(n) & \Box\, \mathit{empty}_X &= \textstyle\bigvee_n F_X(n) & \Simulates{L_n}{Q}{F_Y(n)} \\ \blacklozenge\, \mathit{empty}_Y &= \textstyle\bigvee_n F_Y(n) & \Box\, \mathit{empty}_Y &= \textstyle\bigvee_n F_Y(n) & \Simulates{R_n}{Q}{F_Y(n)} \end{align}\] The first two columns arise by direct observation. The last column holds because every left/right state is simulated by a full state holding the same value.

We derive the fact that if the previous state in the first buffer was a left or right one holding \(n\), then the current state is simulated by an empty state in the second buffer: \[\Simulates{(\blacklozenge\, L_n \lor \blacklozenge\, R_n)}{Q}{\mathit{empty}_Y}\] The derivation proceeds in two symmetric branches, combined by disjunction:

6 Related Work↩︎

A few relational dualities have been previously described in the literature. Most are of the form \(\Op{\CC} \Equiv \DD\) where \(\CC\) is a category whose morphisms are relations, whereas \(\DD\) is a category of algebras with some form of hemimorphism, i.e.a morphism preserving most—but not all!—of the logical structure. The earliest duality of this form is \(\REL \Equiv \CABAJoin\). This duality has been rediscovered multiple times, but is likely due to Jónsson [10]. Kishida [1] argues that this extends to a ‘2-duality,’ as both of these are (strict) 2-categories. Halmos [37] extended it to the continuous case, i.e.a duality between Stone spaces with continuous relations on the one hand, and Boolean algebras with hemimorphisms on the other. Cignoli et al.[38] do something similar for Priestley spaces and continuous monotone relations. Hofmann and Nora [31] have proposed a general framework for such dualities, obtaining the relational side as the Kleisli category of a suitable monad. In later work they extended such dualities to metric structures and quantale-enriched categories [39].

Kurz, Moshier, and Jung [20] present dualities that are much closer to the flavour we employ in this paper. They achieve this by working in an order-enriched setting, where relations can be presented as both spans and cospans in a 2-categorical manner. They use this to extend (well-behaved) dualities to dualities between categories of relations, and even adjunctions of categories to adjunctions between framed bicategories [40]. For example, if their recipe is applied to the category \(\POSET\) of posets and monotone functions it lifts a bimodule \(R : X \relto Y\) to the relation \(\mathbb{2}^R : [X, \mathbb{2}] \relto [Y, \mathbb{2}]\) between upper sets that is defined by letting \(A \Rel{\mathbb{2}^R} B\) just if \(x \in A\) and \(x \Rel{R} y\) implies \(y \in B\). The type of lifting they obtain is very different: as pointed out by one of our reviewers, \(A \Rel{\mathbb{2}^R} B\) just if \(R[A] \subseteq B\), whereas \(A \Lower{R} B\) just if \(A \subseteq R^{-1}[B]\).

Birkmann, Urbat, and Milius [41] present extensions of categorical dualities through monoidal adjunctions and apply them to algebraic language theories. As a corollary they obtain some relational dualities, e.g. between well-behaved relations of profinite ordered monoids and natural morphisms of residuation algebras.

Malacaria [42] presents the Thomason duality in a new light, and shows how it can be used to give bisimulation an algebraic meaning. In particular, the main theorem shows that two Kripke frames are bisimilar just if their associated (dual) algebras have an isomorphic subalgebra.

References↩︎