|
| 1 | +-------------------------- MODULE TransitiveClosure ------------------------- |
| 2 | +(***************************************************************************) |
| 3 | +(* Mathematicians define a relation R to be a set of ordered pairs, and *) |
| 4 | +(* write `s R t' to mean `<<s, t>> \in R'. The transitive closure TC(R) *) |
| 5 | +(* of the relation R is the smallest relation containing R such that, *) |
| 6 | +(* `s TC(R) t' and `t TC(R) u' imply `s TC(R) u', for any s, t, and u. *) |
| 7 | +(* This module shows several ways of defining the operator TC. *) |
| 8 | +(* *) |
| 9 | +(* It is sometimes more convenient to represent a relation as a *) |
| 10 | +(* Boolean-valued function of two arguments, where `s R t' means R[s, t]. *) |
| 11 | +(* It is a straightforward exercise to translate everything in this module *) |
| 12 | +(* to that representation. *) |
| 13 | +(* *) |
| 14 | +(* Mathematicians say that R is a relation on a set S iff R is a subset of *) |
| 15 | +(* S \X S. Let the `support' of a relation R be the set of all elements s *) |
| 16 | +(* such that `s R t' or `t R s' for some t. Then any relation is a *) |
| 17 | +(* relation on its support. Moreover, the support of R is the support of *) |
| 18 | +(* TC(R). So, to define the transitive closure of R, there's no need to *) |
| 19 | +(* say what set R is a relation on. *) |
| 20 | +(* *) |
| 21 | +(* Let's begin by importing some modules we'll need and defining the the *) |
| 22 | +(* support of a relation. *) |
| 23 | +(***************************************************************************) |
| 24 | +EXTENDS Integers, Sequences, FiniteSets, TLC |
| 25 | + |
| 26 | +Support(R) == { r[1]: r \in R} \cup { r[2]: r \in R} |
| 27 | + |
| 28 | +(***************************************************************************) |
| 29 | +(* A relation R defines a directed graph on its support, where there is an *) |
| 30 | +(* edge from s to t iff `s R t'. We can define TC(R) to be the relation *) |
| 31 | +(* such that `s R t' holds iff there is a path from s to t in this graph. *) |
| 32 | +(* We represent a path by the sequence of nodes on the path, so the length *) |
| 33 | +(* of the path (the number of edges) is one greater than the length of the *) |
| 34 | +(* sequence. We then get the following definition of TC. *) |
| 35 | +(***************************************************************************) |
| 36 | +TC(R) == |
| 37 | + LET S == Support( R) |
| 38 | + IN {<<s ,t>> \in S \X S: \E p \in Seq( S): |
| 39 | + /\ Len( p) > 1 |
| 40 | + /\ p[1] = s |
| 41 | + /\ p[ Len( p)] = t |
| 42 | + /\ \A i \in 1 .. ( Len( p) - 1 ): << p[ i], p[ i + 1] >> \in R |
| 43 | + } |
| 44 | + |
| 45 | +(***************************************************************************) |
| 46 | +(* This definition can't be evaluated by TLC because Seq(S) is an infinite *) |
| 47 | +(* set. However, it's not hard to see that if R is a finite set, then it *) |
| 48 | +(* suffices to consider paths whose length is at most Cardinality(S). *) |
| 49 | +(* Modifying the definition of TC we get the following definition that *) |
| 50 | +(* defines TC1(R) to be the transitive closure of R, if R is a finite set. *) |
| 51 | +(* The LET expression defines BoundedSeq(S, n) to be the set of all *) |
| 52 | +(* sequences in Seq(S) of length at most n. *) |
| 53 | +(***************************************************************************) |
| 54 | +TC1(R) == |
| 55 | + LET BoundedSeq(S, n) == UNION {[1 .. i -> S]: i \in 0 .. n} |
| 56 | + S == Support( R) |
| 57 | + IN {<<s ,t>> \in S \X S: \E p \in BoundedSeq( S, Cardinality( S) + 1): |
| 58 | + /\ Len( p) > 1 |
| 59 | + /\ p[1] = s |
| 60 | + /\ p[ Len( p)] = t |
| 61 | + /\ \A i \in 1 .. ( Len( p) - 1 ): << p[ i], p[ i + 1] >> \in R |
| 62 | + } |
| 63 | + |
| 64 | +(***************************************************************************) |
| 65 | +(* This naive method used by TLC to evaluate expressions makes this *) |
| 66 | +(* definition rather inefficient. (As an exercise, find an upper bound on *) |
| 67 | +(* its complexity.) To obtain a definition that TLC can evaluate more *) |
| 68 | +(* efficiently, let's look at the closure operation more algebraically. *) |
| 69 | +(* Let's define the composition of two relations R and T as follows. *) |
| 70 | +(***************************************************************************) |
| 71 | +R ** T == |
| 72 | + LET SR == Support( R) |
| 73 | + ST == Support( T) |
| 74 | + IN {<<r ,t>> \in SR \X ST: \E s \in SR \cap ST: |
| 75 | + ( << r, s >> \in R ) /\ ( << s, t >> \in T ) |
| 76 | + } |
| 77 | + |
| 78 | +(***************************************************************************) |
| 79 | +(* We can then define the closure of R to equal *) |
| 80 | +(* *) |
| 81 | +(* R \cup (R ** R) \cup (R ** R ** R) \cup ... *) |
| 82 | +(* *) |
| 83 | +(* For R finite, this union converges to the transitive closure when the *) |
| 84 | +(* number of terms equals the cardinality of the support of R. This leads *) |
| 85 | +(* to the following definition. *) |
| 86 | +(***************************************************************************) |
| 87 | +TC2(R) == |
| 88 | + LET C[n \in Nat] == |
| 89 | + IF n = 0 THEN R ELSE C[ n - 1] \cup ( C[ n - 1] ** R ) |
| 90 | + IN IF R = {} THEN {} ELSE C[ Cardinality( Support( R)) - 1] |
| 91 | + |
| 92 | +(***************************************************************************) |
| 93 | +(* These definitions of TC1 and TC2 are somewhat unsatisfactory because of *) |
| 94 | +(* their use of Cardinality(S). For example, it would be easy to make a *) |
| 95 | +(* mistake and use Cardinality(S) instead of Cardinality(S)+1 in the *) |
| 96 | +(* definition of TC1(R). I find the following definition more elegant *) |
| 97 | +(* than the preceding two. It is also more asymptotically more efficient *) |
| 98 | +(* because it makes O(log Cardinality (S)) rather than O(Cardinality(S)) *) |
| 99 | +(* recursive calls. *) |
| 100 | +(***************************************************************************) |
| 101 | +RECURSIVE TC3 ( _ ) |
| 102 | +TC3(R) == |
| 103 | + LET RR == R ** R IN IF RR \subseteq R THEN R ELSE TC3( R \cup RR) |
| 104 | + |
| 105 | +(***************************************************************************) |
| 106 | +(* The preceding two definitions can be made slightly more efficient to *) |
| 107 | +(* execute by expanding the definition of ** and making some simple *) |
| 108 | +(* optimizations. But, this is unlikely to be worth complicating the *) |
| 109 | +(* definitions for. *) |
| 110 | +(* *) |
| 111 | +(* The following definition is (asymptotically) the most efficient. It is *) |
| 112 | +(* essentially the TLA+ representation of Warshall's algorithm. *) |
| 113 | +(* (Warshall's algorithm is typically written as an iterative procedure *) |
| 114 | +(* for the case of a relation on a set i..j of integers, when the relation *) |
| 115 | +(* is represented as a Boolean-valued function.) *) |
| 116 | +(***************************************************************************) |
| 117 | +TC4(R) == |
| 118 | + LET S == Support( R) |
| 119 | + RECURSIVE TCR ( _ ) |
| 120 | + TCR(T) == |
| 121 | + IF T = {} |
| 122 | + THEN R |
| 123 | + ELSE LET r == CHOOSE s \in T: TRUE |
| 124 | + RR == TCR( T \ { r }) |
| 125 | + IN RR \cup |
| 126 | + {<<s ,t>> \in S \X S: << s, r >> \in RR /\ << r, t >> \in RR |
| 127 | + } |
| 128 | + IN TCR( S) |
| 129 | + |
| 130 | +(***************************************************************************) |
| 131 | +(* We now test that these four definitions are equivalent. Since it's *) |
| 132 | +(* unlikely that all four are wrong in the same way, their equivalence *) |
| 133 | +(* makes it highly probable that they're correct. *) |
| 134 | +(***************************************************************************) |
| 135 | +ASSUME \A N \in 0 .. 3: |
| 136 | + \A R \in SUBSET ( ( 1 .. N ) \X ( 1 .. N ) ): /\ TC1( R) = TC2( R) |
| 137 | + /\ TC2( R) = TC3( R) |
| 138 | + /\ TC3( R) = TC4( R) |
| 139 | + |
| 140 | +(***************************************************************************) |
| 141 | +(* Sometimes we want to represent a relation as a Boolean-valued operator, *) |
| 142 | +(* so we can write `s R t' as R(s, t). This representation is less *) |
| 143 | +(* convenient for manipulating relations, since an operator is not an *) |
| 144 | +(* ordinary value the way a function is. For example, since TLA+ does not *) |
| 145 | +(* permit us to define operator-valued operators, we cannot define a *) |
| 146 | +(* transitive closure operator TC so TC(R) is the operator that represents *) |
| 147 | +(* the transitive closure. Moreover, an operator R by itself cannot *) |
| 148 | +(* represent a relation; we also have to know what set it is an operator *) |
| 149 | +(* on. (If R is a function, its domain tells us that.) *) |
| 150 | +(* *) |
| 151 | +(* However, there may be situations in which you want to represent *) |
| 152 | +(* relations by operators. In that case, you can define an operator TC so *) |
| 153 | +(* that, if R is an operator representing a relation on S, and TCR is the *) |
| 154 | +(* operator representing it transitive closure, then *) |
| 155 | +(* *) |
| 156 | +(* TCR(s, t) = TC(R, S, s, t) *) |
| 157 | +(* *) |
| 158 | +(* for all s, t. Here is the definition. (This assumes that for an *) |
| 159 | +(* operator R on a set S, R(s, t) equals FALSE for all s and t not in S.) *) |
| 160 | +(***************************************************************************) |
| 161 | +TC5(R ( _ , _ ), S, s, t) == |
| 162 | + LET CR[n \in Nat, |
| 163 | + v \in S] == |
| 164 | + IF n = 0 |
| 165 | + THEN R( s, v) |
| 166 | + ELSE \/ CR[ n - 1, v] |
| 167 | + \/ \E u \in S: CR[ n - 1, u] /\ R( u, v) |
| 168 | + IN /\ s \in S |
| 169 | + /\ t \in S |
| 170 | + /\ CR[ Cardinality( S) - 1, t] |
| 171 | + |
| 172 | +(***************************************************************************) |
| 173 | +(* Finally, the following assumption checks that our definition TC5 agrees *) |
| 174 | +(* with our definition TC1. *) |
| 175 | +(***************************************************************************) |
| 176 | +ASSUME \A N \in 0 .. 3: |
| 177 | + \A R \in SUBSET ( ( 1 .. N ) \X ( 1 .. N ) ): |
| 178 | + LET RR(s, t) == << s, t >> \in R |
| 179 | + S == Support( R) |
| 180 | + IN \A s, t \in S: |
| 181 | + TC5( RR, S, s, t) <=> ( << s, t >> \in TC1( R) ) |
| 182 | +============================================================================= |
0 commit comments