Proof of algorithm for non-strict comparisons

We now prove that the revised algorithm presented in section 6.2 for non-strict comparisons is correct. The proof is only a slight extension of the proof of theorem 1, given above. Recall that the revised algorithm in section 6.2 replaces the line of solve_constraints

H := the connected components of the shorts of S

with the following code:

1.   H := the shorts of S; 
2.   repeat H := the connected components of H;
3.          for each weak constraint od(a,b) <<= od(c,d)
4.              if cd is in H then add ab to H endif endfor
5.   until no change has been made to H in the last iteration.

We need the following new lemmas and proofs:

Lemma 20:  Let S be a set of strict comparisons, and let W be a set of non-strict comparisons. Let H be the set of edges output by the above code. If S union W is consistent, then there is an edge in S that is not in H.

Proof: As in the proof of lemma 5, let Z be a valuation satisfying S union W and let pq be an edge in S such that od( Z(p), Z(q)) is maximal. We wish to show that, for every edge ab in H, od( Z(a), Z(b)) << od( Z(p), Z(q)), and hence ab <> pq. Proof by induction: suppose that this holds for all the edges in H at some point in the code, and that ab is now to be added to H. There are three cases to consider.

• ab is added in step [1]. Then, as in lemma 5, there is a constraint od(a,b) << od(c,d) in S. Hence od( Z(a), Z(b)) << od( Z(c), Z(d)) <<= od( Z(p), Z(q)).

• ab is added in step [2]. Then there is a path a₁=a, a₂ ... a_k =b such that the edge a_ia_i+1 is in H for i=1 ... k-1. By the inductive hypothesis, od( Z(a_i),Z(a_i+1)) << od(Z(p),Z(q)). By the om-triangle inequality, od( Z(a), Z(b)) <<= max_{i=1 .. k-1}(od (Z(a_i), Z(a_i+1))) <<od( Z(p), Z(q)).

• ab is added in step [4]. Then there is a constraint od(a,b) <<= od(c,d) in W such that cd is in H. By the inductive hypothesis, od( Z(c), Z(d)) << od( Z(p), Z(q)).

Lemma 21:  Let W contain the constraint od(a,b) <<= od(c,d). Suppose that the algorithm returns a cluster tree T. Let M be the least common ancestor of a and b in T, and let N be the least common ancestor of c and d. Then M.label <= N.label.

Proof: By lemma 13, N is assigned a label in the first iteration where H does not include the edge cd. In all previous iterations, since cd is in H, ab will likewise be put into H. Hence M does not get assigned a label before N, so M.label <= N.label.

The remainder of the proof of the correctness of the revised algorithm is exactly the same as the proof of theorem 1.