Relating Domain Concepts Intensionally by Ordering Connections - Formal Methods and Hybrid Real-Time Systems - page 192

Definition 5 (Information Flow Connection). By an information flow con-
nection , we understand a relation between domain concepts appearing in different
stages of an information flow. The connection states how one kind of information
serves as input to the creation and elaboration of other kinds of information.

In this paper, we shall consider the information flow connection between objects
representing the information on different stages of projects. However, the notion
is applicable in many other domains.
In the following, we shall consider the theoretical foundation of these two
kinds of connections.

3.1 Galois Connections and Abstract Interpretation

Formulated in RSL, the definition of Galois connections is:

Definition 6 (Galois Connection). A Galois connection is a dual pair of
mappings ( F , G ) between two ordered sets ( P, ≤ ) and ( Q, ≤ ) . Most often the

ordering is based on set-inclusion ( ) and this is also the version we shall use

here. The mappings must be monotonously decreasing 2 :

⊆

type
P, Q

value
F :P-set → Q-set

G →

:Q-set P-set

axiom
∀ ps 1 ,ps 2 :P-set,qs 1 ,qs 2 :Q-set •
ps 1 ⊆ ps 2 ⇒F ps 2 ⊆F ps 1 ,
qs 1 ⊆ qs 2 ⇒G qs 2 ⊆G qs 1 ,
ps 1 ⊆GF ps 1 ,

qs 1 ⊆FG qs 1

In [1], the following Theorem is given on Galois connections (here omitting the
proof):

Theorem 1 (Galois Connection 3 ). For every binary relation R ⊆ M × N ,a

Galois connection ( ϕ R ,ψ R ) between M and N is defined by

ϕ R X := X R (= y ∈ N | xRy f or all x ∈ X )

ϕ R Y := Y R (= x ∈ M | xRy f or all y ∈ Y ) .

2 Note, that there are in fact two different definitions of Galois connections in the
literature: the monotone Galois connection and the antitone Galois connection. We
follow Ganter and Wille by assuming the former [1].
3 In[1]thisisnamedTheorem2.