= Well-founded progress in recursion
{title2=$\mu(\text{child})<\mu(\text{parent})$}
A <base case> and a decreasing <natural number> measure work together. Check that every invocation satisfies its <precondition>, each <base case> finishes with the correct <output>, and every other invocation makes finitely many <recursive calls> with strictly smaller measure. All local work must also terminate. By <well-founded induction>, the children finish, so their caller finishes; if their answers are correct and the combination rule preserves the <postcondition>, the caller is correct too. This proves <total correctness>, not just correctness conditional on return.
Strict decrease without a lower bound is insufficient: subtracting one forever from a negative <integer> never reaches zero. Even a positive real-valued measure can decrease indefinitely, as $1,1/2,1/4,\ldots$ shows. A <well-founded relation> rules out that descent. In <structural recursion>, a proper child <subtree> of a finite <binary tree> supplies progress without numeric arguments. The proof obligation is the relation between parent and child instances, together with terminating local work and complete <base cases>.
Back to article page
