Part of a presentation on Coalgebras over Lawvere Metric Spaces

Generalising to Ordered Sets

We write

$Ord$ for the category

$Pre$ of preorders or

$Pos$ or partial orders if we wish to emphasize that the concepts and results do not depend on the specific choice.

Coalgebras over Orders

How can we formalize only one half of a bisimulation using the coalgebras? In other words, how can we account for simulation instead of bisimulation?

The solution is to equip the final coalgebra with a preorder that accounts for simulation. Technically, this means that we look at coalgebras for a functor

$T:Ord\to Ord$. Moreover, we need to assume that

$T$ is locally monotone, that is,

$T$ preserves the order on hom-sets. In other words, we are now moving our attention from ordinary category theory to

$Ord$-enriched category theory.

While there is a uniform definition of

$T$-simulation for all functors

$T:Ord\to Ord$, we only look at the paradigmatic example of the powerset functor.

Example: Let

$\mathcal{P}:Pre\to Pre$ be the functor that takes a preorder to all its subsets. The order on subsets can be defined in three different ways. Let

$a,b\in \mathcal{P}X$.

• (forward simulation) We write
  ${\mathcal{P}}^{\downarrow }X$ if the order is defined as
  
  $$a⊑b\iff \mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y$$
• (backward simulation) We write
  ${\mathcal{P}}^{\uparrow }X$ if the order is defined as
  
  $$a⊑b\iff \mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y$$
• (bisimulation) We write
  ${\mathcal{P}}^{c}X$ if the order is defined by the conjunction of the two clauses above.

Remark: It is not difficult to show that if one quotients preorders to posets then one can identify

${\mathcal{P}}^{\downarrow }X$ with the downsets,

${\mathcal{P}}^{\uparrow }X$ with the upsets, and

${\mathcal{P}}^{c}X$ with the convex subsets of

$X$.

Remark: The coalgebra morphisms of

${\mathcal{P}}^{\downarrow }$,

${\mathcal{P}}^{\uparrow }$ and

${\mathcal{P}}^c$ give rise, respectively, to forward, backward, bi-simulation.

Summary: I only had time to show with the help of the paradigmatic example how the move from set-based to order-based coalgebras corresponds to the move from bisimulation to simulation. Of course, much work is required to show that the rich theory of set-based coalgebras generalises and extends to this setting.

Coalgebraic Logic over Orders

Suffice it to say that the adjunction we used for coalgebras over set has an ordered version

Going back to our summary of coalgebraic logic over sets, the expectation would be that all results have an ordered generalisations but the details are more tricky and not all results have been generalised so far.

References

In a sense most of the work in domain theory could be seen as an example of what we discussed in this section. But the particular flavour of domain theory comes from studying a wide variety of sophisticated ordered structures to obtain final coalgebras for functors (such as

$X\mapsto X^X$) which cannot be treated in the simple setting of this note. On the other hand there are many examples that do not need the more complicated apparatus of domain theory.

Simulation for coalgebras was studied in

• Jesse Hughes, Bart Jacobs: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2): 71-108 (2004)

Algebra and coalgebra over ordered sets has been explored in the following of my publications.

• Alexander Kurz, Andrew Moshier, Achim Jung: Stone Duality for Relations. 2019, submitted. (pdf)
• A Kurz, J Velebil: Quasivarieties and varieties of ordered algebras: Regularity and exactness. Mathematical Structures in Computer Science 27(7): 1153-1194 (2017). (pdf)
• Dahlqvist, Fredrik ; Kurz, Alexander: The Positivication of Coalgebraic Logics. CALCO 2017
• A Balan, A Kurz, J Velebil: Positive Fragments of Coalgebraic Logics. Logical Methods in Computer Science, Vol. 11(3:18)2015, pp. 1–51 (pdf).
• K. Kapulkin, A. Kurz, J. Velebil: Expressiveness of Positive Coalgebraic Logic. Advances in Modal Logic 2012 (pdf)
• M. Bilkova, A. Kurz, D. Petrisan, J. Velebil: Relation Liftings on Preorders and Posets. CALCO'11 Updated version with proofs, September 2012.
• A Balan, A Kurz: Finitary Functors: From Set to Preord and Poset. CALCO'11