LARA

Lab 02 - Relations

In this lab we'll practice some (more formal) proofs, hence show all steps in the exercises.
You may find the pages on First-order logic and Sets and Relations helpful.

Exercise 1 - Relations, a warm up

Prove the following or give a counterexample.

  1. $(r \cup s) \circ t = ( r \circ t) \cup (s \circ t)$
  2. $(r \cap s) \circ t = (r \circ t) \cap (s \circ t)$
  3. $(r_1 \circ r_2)^{-1} = (r_2^{-1} \circ r_1^{-1})$
  4. $S \bullet r = ran(\bigtriangleup_S \circ r)$
  5. If $r_1 \subseteq r_1'$ then $r_1 \circ r_2 \subseteq r_1' \circ r_2$ and $r_2 \circ r_1 \subseteq r_2 \circ r_1'$.
  6. If $r_1 \subseteq r_1'$ then $r_1 \cup r_2 \subseteq r_1' \cup r_2$ and $r_2 \cup r_1 \subseteq r_2 \cup r_1'$.

Note that the last two properties, if they hold, specify that relation composition and union are monotone.

Exercise 2 - Monotonicity

Let $E(r_1, r_2, ..., r_n)$ be a relation composed of relations $r_i$ with an arbitrary combination of relation composition and union, that is the expressions $E$ are trees with leaves being relations $r_i$. Show that this operation is monotone, that is show that for any $i$ $r_i \subseteq r_i' \quad \rightarrow \quad E(r_1, r_2, ..., r_i, ... , r_n) \subseteq E(r_1, r_2, ..., r_i', ... , r_n) $.
As an illustration, one possible expression could be $(r_1 \circ r_2) \cup r_3$, then if $r_2 \subseteq r_2'$ then $(r_1 \circ r_2) \cup r_3 \subseteq (r_1 \circ r_2') \cup r_3$.

Solution

Exercise 3 - Relation of an entire program

Compute the relations for these programs. The final formulas cannot be expressed in Presburger arithmetic, for the sake of this exercise we'll allow any arithmetic you seem fit. 

  x = x * y
  if (z > 5) {
    y = y + x
    x += 1
  } else {
    havoc(z)
    y = y - x
  }
  while ( x < 100 ) {
    y = y + 1
    x = x * 2
  }

Exercise 4 - Transitive closure

Suppose $r \subseteq A\times A$. Show that the following 4 definitions of transitive closure are equivalent:

  1. $r^* = \bigcup_{n \geq 0} r^n$
  2. the least relation $s$ (with respect to $\subseteq$) that satisfies: $ \Delta_A\ \cup\ (s \circ r)\ \subseteq\ s $
  3. the least relation $s$ (with respect to $\subseteq$) that satisfies: $\Delta_A\ \cup\ (r \circ s)\ \subseteq\ s$
  4. the least relation $s$ (with respect to $\subseteq$) that satisfies: $\Delta_A\ \cup\ r \cup (s \circ s)\ \subseteq\ s$

Partial solution