
## End Incorporate Order

Function incorporate order serves the following purpose.  Suppose that we are in the midst of the main loop of solve constraints 2, we have a partially constructed cluster tree, and we are currently working on finding the sub-clusters of a node N . As in the original form of solve constraints, we find the connected components of the shorts of the order-ofmagnitude constraints. Let these be C 1 . . . C g ; then we know that the diameter of each C i is much smaller than the diameter of N . Now, suppose, for example, that we have in O the constraints a 1 < a 5 , b 5 < b 2 , c 2 < c 1 , where a 1 , c 1 E C 1 ; b 2 , c 2 E C 2 ; and a 5 , b 5 E C 5 . Then it follows from axiom A.9 that C 1 , C 2 , and C 5 must all be merged into a single cluster, whose diameter will be less than the diameter of N . Procedure incorporate order finds all such loops by constructing a graph G whose vertices are the connected components of H and whose arcs are the ordering relations in O and then computing the strongly connected components of G. (Recall that two vertices u, v in a directed graph are in the same strongly connected component if there is a cycle from u to v to u.) It then merges together all of the connected components of H that lie in a single strongly connected component of G .

The proof of the correctness of algorithm solve constraints2 is again analogous in structure to the proof of theorem 1, and is given in the appendix.

By implementing this in the manner of Section 6.1, the algorithm can be made to run in time O (max(n²α(n), ne, no, s)), where o is the number of constraints in O .

## 7. Finite Order Of Magnitude Comparison

In this section, it is demonstrated that algorithm solve constraints can be applied to systems of constraints of the form "dist( a, b ) < dist( c, d ) / B " for finite B in ordinary Euclidean space as long as the number of symbols in the constraint network is smaller than B .

We could be sure immediately that some such result must apply for finite B . It is a fundamental property of the non-standard real line that any sentence in the first-order theory of the reals that holds for all infinite values holds for any sufficiently large finite value, and that any sentence that holds for some infinite value holds for arbitrarily large finite values. Hence, since the answer given by algorithm solve constraints works over a set of constraints S when the constraint "od(a, b) « od(c, d)" is interpreted as "od(a, b) < od( c, d )/B for infinite B ", the same answer must be valid for sufficiently large finite B .

What is interesting is that we can find a simple characterization of B in terms of S ; namely, that B is larger than the number of symbols in S .

We begin by modifying the form of the constraints, and the interpretation of a cluster tree. First, to avoid confusion, we will use a four-place predicate "much_closer(a, b, c, d)"
rather than the form "od(a, b) « od(c, d)" as we are not going to give an interpretation to
"od" as a function. We fix a finite value B > 1, and interpret "much_closer(a, b, c, d)" to mean "dist(a, b) < dist(c, d) / B ."
We next redefine what it means for a valuation to instantiate a cluster tree:
Definition 6: Let T be a cluster tree and let Γ be a valuation on the symbols in T .  We say that Γ ├ T if the following holds: For any symbols a, b, c, d in T , let M be the least common ancestor of a, b and let N be the least common ancestor of c, d. If M .label < N .label then much_closer( a, b, c, d ).