242 (transitive closure) A relation R: (0,..n)→(0,..n)→bin can be represented by a square binary array of size n . Given a relation in the form of a square binary array, write a program to find
(a) its transitive closure (the strongest transitive relation that is implied by the given relation).
§ Let Pijk mean “there is a path in R from j to k via zero or more intermediate nodes all of which are less than i ”. Formally,
P0 = R
∀i, j, k· P(i+1)jk = Pijk ∨ Piji ∧ Piik
Then we can say that Rʹ is the transitive closure of R as follows:
Rʹ = Pn
This is just right for a for-loop (Chapter 5).
R=P0 ⇒ Rʹ=Pn ⇐ for i:= 0;..n do R=Pi ⇒ Rʹ=P(i+1) od R=Pi ⇒ Rʹ=P(i+1) ⇐
for j:= 0;..n do for k:= 0;..n do R:= (j;k) → Rjk ∨ Rji ∧ Rik | R od od That’s the whole thing. If you want more detail, define A as follows.
Aijk =
∧
∧ ∧
(∀r: 0,..j· ∀c: 0,..n· Rrc=P(i+1)rc) (∀c: 0,..k· Rjc=P(i+1)jc)
(∀c: k,..n· Rjc=Pijc)
(∀r: j+1,..n· ∀c: k,..n· Rrc=Pirc)
00 k n j
j+1 n
Now Ai00 = R=Pi and Aijn = Ai(j+1)0 and Ain0 = A(i+1)00 . A000 ⇒ Aʹn00 ⇐ for i:= 0;..n do Ai00 ⇒ Aʹ(i+1)00 od Ai00 ⇒ Aʹ(i+1)00 ⇐ for j:= 0;..n do Aij0 ⇒ Aʹi(j+1)0 od Aij0 ⇒ Aʹi(j+1)0 ⇐ for k:= 0;..n do Aijk ⇒ Aʹij(k+1) od Aijk ⇒ Aʹij(k+1) ⇐ R:= (j;k) → Rjk ∨ Rji ∧ Rik
Of course, for-loops are not necessary.
(b) its reflexive transitive closure (the strongest reflexive and transitive relation that is implied by the given relation).
§ This is similar to part (a), but this time we define P0jk = j=k ∨ Rjk . Since P0 is not true initially, we need to start with
Rʹ=Pn ⇐ for j:= 0;..n do R:= (j;j) → ⊤ | R od. R=P0 ⇒ Rʹ=Pn
and then continue as before.
P(i+1)
Pi