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:

procedureinstantiate(inT: cluster tree;O: Euclidean space;B: real);return: array of points indexed on the symbols ofT;Let

nbe the number of nodes inT;a:= 2 + 2n+Bn; Choosed_{1},d_{2}...d_{n}such thatd_{i}<d_{i+1}/a; pick a pointx in O;G[T]:=x; instantiate1(T,O,d_{1}...d_{n},G);returnthe restriction ofGto the symbols ofT.endinstantiate.

instantiate1(inN: a node in a cluster tree;O: a Euclidean space;d_{1}...d_{n}: orders of magnitude;in outG : array of points indexed on the nodes ofT)ifNis not a leafthenletC_{1}...C_{p}be the children ofN;x_{1}:=G[N];q:=N.label; pick pointsx_{2}...x_{p}such that for alli,jin 1 ...p, ifi<>jthend_{q}<= dist(x_{i},x_{j}) <n d_{q}/* This is possible sincep<=n. */fori= 1 ...pdoG[C_{i}]:=x_{i}; instantiate1(C_{i},O,d_{1}...d_{n},G)endforendifendinstantiate1.

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.