[Solved]: How to prove that the pre-order tree traversal algorithm terminates?

Problem Detail: 

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?

Asked By : xando

Answered By : Joe

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...

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/4719