User Manual for Rodin v.2.3: Relations

2.5.5 Relations

Relations are a powerful instrument when modeling systems. From a mathematical point of view a relation is just a set of pairs. Formally, when we have to sets $A$ and $B$ , we can specify that $r$ is a relation between both by $r \in \mathop {\mathbb P\hbox{}}\nolimits (A\mathbin \times B)$ (ASCII: r:POW(A**B)). Because relations are so common, we can write it shorter $r \in A\mathbin \leftrightarrow B$ (ASCII: r:A<->B).

With $a\mapsto b\in r$ , we can check if two elements $a$ and $b$ are related in respect to $b$ .

We use a small example to illustrate relations. Let $A = \{ a,b,c,d\}$ and $B=\{ 1,2,3,4\}$ . We define the relation $r$ with $r = \{ a\mapsto 1, a\mapsto 3, c\mapsto 2, d\mapsto 1\}$ . The domain of $r$ are all elements occurring on the left side $\mathop {\mathrm{dom}}\nolimits (r) = \{ a,c,d\}$ and the range are all elements on the right $\mathop {\mathrm{ran}}\nolimits (r)=\{ 1,2,3\}$ .

To find out to which elements the objects of the set $s=\{ b,c,d\}$ are related to, we can use the relational image: $r[s] = r[\{ b,c,d\} ] = \{ 1,2\}$ . Often we want to know to which object a single element $b$ is related. We just write it as a singleton set: $r[\{ a\} ] = \{ 1,3\}$ .

Event-B supports several operators to work with relations. (3.3.5) We will not go into more detail during the course of the tutorial.

An important special case of relations are functions. Functions are relations where each element of the domain is uniquely related to one element of the range. Event-B directly supports operators to describe partial and total functions, which can injective, surjective or bijective.

Rodin Handbook

2.5.5 Relations