# 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)))