Rodin User’s Handbook v.2.8: Relations

2.5.5 Relations

Relations are a powerful instrument when modelling systems. From a mathematical point of view, a relation is just a set of pairs. Formally, when we have two 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, there is also a symbol to denote a relation, so a shorter way to write the above expression is $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 $a$ 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 be injective, surjective or bijective.

Rodin Handbook

2.5.5 Relations