next up previous
Next: Validation of algorithm solve_constraints2 Up: Appendix A. Proofs Previous: Proof of Theorem 2

   
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.

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.


next up previous
Next: Validation of algorithm solve_constraints2 Up: Appendix A. Proofs Previous: Proof of Theorem 2