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

Question

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?

Answer 1

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