# How to prove that the pre-order tree traversal algorithm terminates?

I see structural induction the usual way for proving an algorithm's termination property, but it's not that easy to prove by means of induction on a tree algorithm. Now I am struggling on proving that the pre-order tree traversal algorithm is terminable:

preorder(node)
if node == null then return
visit(node)
preorder(node.left)
preorder(node.right)


How should I prove?

Hint (by Raphael): How do you prove that the recursive factorial function terminates?

Answer (by Kejia): The recursive factorial function's universe is non-negative integers, which is countable and so well-found, and so it is very easy to prove with mathematical induction.

By analogy, we can find a mapping from trees to a well-founded universe so that a similar proof works.

Our mapping is to the size of the subtree. At each recursive call, the size of a subproblem (i.e. a subtree) is strictly decreasing and always non-negative. Therefore, we can proceed by induction.

Suppose (induction hypothesis) that the function on a tree of size of at most k terminates. Now consider an input tree with k+1 nodes...

• Why is that sufficient? (I know the answer, but your post is a bit thin.)
– Raphael
Sep 25, 2012 at 6:00
• @Joe yes, and how to prove?
– 象嘉道
Sep 25, 2012 at 14:47