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 Z be a valuation on the symbols in T. We say that Z satisfies 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).

Procedure ``instantiate'', which generates an instantiation of a cluster tree, is modified as follows:

procedure instantiate(in T : cluster tree; O : Euclidean space; B : real);
		      return : array of points indexed on the symbols of T;

Let n be the number of nodes in T; 
a := 2 + 2n + Bn; 
Choose d1, d2 ... dn such that di < di+1 / a; 
pick a point x in O; 
G[T] := x; 
instantiate1(T,O, d1 ... dn, G); 
return the restriction of G to the symbols of T. 
end instantiate. 

instantiate1(in N : a node in a cluster tree; O : a Euclidean space; 
		d1 ... dn : orders of magnitude; 
	     in out G : array of points indexed on the nodes of T) 
if N is not a leaf then
     let C1 ... Cp be the children of N; 
     x1 := G[N]; 
     q := N.label;
     pick points x2 ... xp such that
          for all i,j in 1 ... p, if i <> j then dq <= dist(xi, xj) < n dq
     /* This is possible since p <= n. */
     for i = 1 ... p do
	  G[Ci] := xi;
          instantiate1(Ci, O, d1 ... dn, G)
     endfor
endif end instantiate1.

The analogue of lemma 2 holds for the revised algorithm:

Lemma 22:  Any cluster tree T has an instantiation in Euclidean space R^m of any dimensionality m.

We can now state theorem 3, which asserts the correctness of algorithm ``solve_constraints'' in this new setting:

Theorem 3:  Let S be a set of constraints over n variables of the form ``dist(a,b) < dist(c,d) / B'', where B > n. The algorithm solve_constraints(S) returns a cluster tree satisfying S if S is consistent over Euclidean space, and returns false if S is inconsistent.

The proofs of lemma 22 and theorem 3 are given in the appendix.

An examination of the proof of lemma 22 shows that this result does not depend on any relation between n and B. Therefore, if solve_constraints(S) returns a tree T, then S is consistent and T satisfies S regardless of the relation between n and B. However, it is possible for S to be consistent and solve_constraints(S) to return false if n >= B. On the other hand, one can see from the proof of theorem 3 (particularly lemma 23) that if B > n and solve_constraints(S) returns false then S is inconsistent in any metric space. However, there are metric spaces other than R^m in which the cluster tree returned by solve_constraints may have no instantiation.