Try   HackMD

Montone Neighbourhood Coalgebras

(draft) (up)

Introduction

The idea of this section is to run through parts of [HK04] and adapt it to ordered neighbourhood frames. It could also be interesting to study metric neighbourhood frames.

The neighbourhood frames of modal logic are coalgebras for the functor

UpP [HK04,Lem.3.4]. Here,
UpPX={AP(PX)aA,aaaA}
. On functions, we have
UpP f A={f[a]aA}.

There are three well-known ways of extending powerset to orders. In domain theory, they are known as the upper, lower and convex powerdomain, and also known under the names of Hoare, Smyth and Plotkin, respectively. They correspond to the downset functor

D, the upset functor
U
and the convex powerset functor
P
. The first two arise from ordering powerset by inclusion and reverse inclusion. The third arises as the posetification of the powerset.

Similarly, there are three ways to extend the monotone neighbourhood functor

UpP to posets.

Recall that on objects

UX=[X,2]o and
DX=[Xo,2]
. As a functor (and as a monad)
DUX=[[X,2],2]

and

UDX=[[Xo,2],2]o.

On discrete

X, we have
DUX=(UDX)o
, so both are legitimate order generalisations of the functor
UpP
.

Finally, there is also the posetification

UpP.

We derive the notions of cospan (bi)simulation of the functors

DU and
UD
and
UpP
.

Coalgebra Morphisms

Proposition:

f is a morphism of
DU
-coalgebras iff
aξx.bν(fx).yb.xa.fxybν(fx).aξ(x).xa.yb. yfx

f is a morphism of
DU
-coalgebras iff

aξx.bν(fx).yb.xa.fxybν(fx).aξx.xa.yb.yfx

f is a morphism of
UpP
-coalgebras if

Morphisms of

DU and
UD
-coalgebras coincide on discrete coalgebras. Here is an attempt at a visual summary:

Image Not Showing Possible Reasons
  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported
Learn More →

Morphisms as Relations

In sets every function is a relation and every coalgebra morphism a bisimulation. In ordered sets every function

f:XY gives rise to two relation
f:XY
and
f:YX
with
(x,y)f  fxy(y,x)f  yfx

We have shown in Cospan Bisimulations 2 that these relations are cospan (bi)simulations if

f is a coalgebra morphism. This example suggests that more is true.

Proposition:

f is a morphism of
DU
-coalgebras iff
f
and
f
are cospan-(bi)simulations.

Proof: We only need to instantiate the characterisation of

DU-cospan-(bi)simulation from the section on Bisimulation for Ordered Coalgebras.

An analogous statement is true for

UD-coalgebras (CHECK).

Image Not Showing Possible Reasons
  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported
Learn More →

(WHERE DO WE SEE THE DIFFERENCE BETWEEN THE TYPES OF COALGEBRAS IN THE LOGICS?)

Def: The two-sorted modal logic for ordered neighbourhood frames has point-formulas

ϕ and set-formulas
ψ
given as

ϕ::=ψϕϕϕϕpψ::=ϕψψψψ

and axioms saying that

preserves finite meets and
preserves finite joins.

Remark: This logic can be derived from the semantics using the principles of functorial modal logic (FML). This construction then guarantees the following proposition.

Prop: Formulas are invariant under morphisms and behavioural equivalence. Moreover, the logic is sound and complete for ordered neighbourhood models.

References

Dahlqvist and Kurz: The Positivication of Coalgebraic Logics. CALCO 2017. (Section 3.3 and 3.4)

Hansen, Kupke: A Coalgebraic Perspective on Monotone Modal Logic. 2004.

M. Pauly. Bisimulation for general non-normal modal logic. Manuscript, 1999.