Termination of tree rotations

A tutorial problem for the course Algorithms and Data Structures asks for a proof that tree rotations can transform a binary tree into any other tree of the same size with the nodes in the same infix order. The suggested argument is that one tree can be transformed into the other via a normal form, such as a rightward-pointing spine.

The lecturer's answer suggests an algorithm for transforming any tree to normal form: find a node (perhaps the rightmost one) on the spine that has a left child, rotate it to the right, and repeat until there are no more nodes with left children. It's clear that, if this algorithm terminates, it does so in a state where the tree has been reduced to a rightward-pointing spine as desired. But can we be sure of termination? The model answer says only that in each step one node has reached its "correct position," but I don't quite know what that means. A clearer argument might be to exhibit a bound function, non-negative for every tree, that is reduced in each rotation. Such a bound function is the number of nodes that are not on the spine, that is, the total size of all left subtrees of nodes on the spine. This function is clearly non-negative, and it decreases by one whenever a node on the spine is rotated to the right.

A script for the Boyer-Moore theorem prover follows. For simpicity, we will treat binary trees with labelled leaves but unlabelled internal nodes, because this variation on trees is provided by the LISP-like s-expressions already present in the prover.

After resetting the theorem prover to its ground-zero state, we begin by defining a predicate normp that tests whether its argument is in our desired normal form.

(boot-strap)

(defn normp (x)
  (if (nlistp x) t
    (and (nlistp (car x)) (normp (cdr x)))))

Our challenge is to get the prover to accept our proposed definition of normalise, because the prover checks that each function is total before accepting its definition. To that end, we begin be defining a function step that performs one step of normalisation, searching for the highest node in the spine that has a non-trivial left subtree, and rotating it.

(defn step (x)
  (if (nlistp x) x
    (if (nlistp (car x))
        (cons (car x) (step (cdr x)))
      (cons (caar x) (cons (cdar x) (cdr x))))))

We must now define a measure cost that is reduced by step when applied to a tree that is not in normal form. As suggested above, we define it as the sum of the sizes of all left subtrees of nodes on the spine.

(defn size (x)
  (if (nlistp x) 0
    (plus (size (car x)) (size (cdr x)) 1)))

(defn cost (x)
  (if (nlistp x) 0
    (plus (size (car x)) (cost (cdr x)))))

It is a straightforward induction to prove that step does reduce cost as we want.

(prove-lemma cost-step (rewrite)
  (implies (not (normp x))
           (lessp (cost (step x)) (cost x))))

That gives us what we need to bully the prover into accepting our definition of normalise, which we do by giving it a hint that it should prove termination by using the measure (cost x) and the well-founded relation lessp.

(defn normalise (x)
  (if (normp x) x
    (normalise (step x)))
  ((lessp (cost x))))

We can eaily prove the normalise returns a tree in normal form.

(prove-lemma normalise-is-normp (rewrite)
  (normp (normalise x)))

An alternative algorithm norm1 for normalising a tree is to work our way up the right spine, recursively grinding each left subtree into atoms that we cons onto the spine.

(defn grind (x y)
  (if (nlistp x)
      (cons x y)
    (grind (car x) (grind (cdr x) y))))

(defn norm1 (x)
  (if (nlistp x) x
    (grind (car x) (norm1 (cdr x)))))

This function returns the same result as normalise, as we can prove in stages. First, we must prove the technical result that if its input is already in normal form, then norm1 returns it unchanged.

(prove-lemma normp-norm1 (rewrite)
  (implies (normp x)
           (equal (norm1 x) x)))

Also, norm1 applied to (step x) gives the same result as norm1 applied to x: that means that as normalise transforms its input step-by-step, the normal form as returned by norm1 does not change.

(prove-lemma norm1-step (rewrite)
  (equal (norm1 (step x)) (norm1 x)))

An easy induction is all that is now needed to show that norm1 and normalise are the same.

(prove-lemma norm1-is-normalise (rewrite)
  (equal (norm1 x)
         (normalise x)))