Structural induction

Structural induction is a proof method that is used in mathematical logic (e.g., the proof of Los's theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction.
In general, the idea is that one wishes to prove some proposition P(x), where x is any instance of some sort of recursivelydefined structure such as lists or trees. A wellfounded partial order is defined on the structures. The structural induction proof then consists of proving that the proposition holds for all the minimal structures, and that if it holds for the substructures of a certain structure S, then it must hold for S also. For example, if the structures are lists, one usually introduces the partial order '<' in which L < M whenever list L is the tail of list M. Under this ordering, the empty list [] is the unique minimal element. A structural induction proof of some proposition P(l) then consists of two parts: A proof that P([]) is true, and a proof that if P(L) is true for some list L, and if L is the tail of list M, then P(M) must also be true.
Example
Consider the following property of lists:
length (L ++ M) = length L + length M [EQ]
Here ++ denotes the list append operation.
In order to prove this, we need definitions for length and for the append operation.
length [] = 0 [LEN1] length (h:t) = 1 + length t [LEN2]
[] ++ list = list [APP1] (h:t) ++ list = h: (t ++ list) [APP2]
Here (h:t) denotes a list whose head is h and whose tail is t. Our proposition P(l) is that EQ is true for all lists M when L is l. We want to show that P(l) is true for all lists l. We will prove this by structural induction on lists.
First we will prove that P([]) is true; that is, EQ is true for all lists M when L happens to be the empty list []. Consider EQ:
length (L ++ M) = length L + length M length ([]++ M) = length [] + length M length M = length [] + length M (by APP1) length M = 0 + length M (by LEN1)
So this part of the theorem is proved; EQ is true for all M, when L is [], because the lefthand side and the righthand side are equal.
Now we will prove P(l) when l is a nonempty list. Since l is nonempty, it has a head item, x, and a tail list, xs, so we can express it as (x:xs). The induction hypothesis is that EQ is true for all values of M when L is xs:
length (xs ++ M) = length xs + length M (hypothesis)
We would like to show that if this is the case, then EQ is also true for all values of M when L is a list x:xs whose tail is xs. We proceed as before:
length (L ++ M) = length L + length M length ((x:xs)++ M) = length (x:xs) + length M length (x:(xs ++ M)) = length (x:xs) + length M (by APP2) 1 + length (xs ++ M) = length (x:xs) + length M (by LEN2) 1 + length (xs ++ M) = 1 + length xs + length M (by LEN2) length (xs ++ M) = length xs + length M
As this is just the induction hypothesis, we're done.
WellOrdering
Just as standard mathematical induction is equivalent to the wellordering principle, structural induction is also equivalent to a wellordering principle. If the set of all structures of a certain kind admits a wellfounded partial order, then every nonempty subset must have a minimal element. (This is the definition of "wellfounded".) The significance of the lemma in this context is that it allows us to deduce that if there are any counterexamples to the theorem we want to prove, then there must be a minimal counterexample. If we can show the existence of the minimal counterexample implies an even smaller counterexample, we have a contradiction (since the minimal counterexample isn't minimal) and so the set of counterexamples must be empty.
As an example of this type of argument, consider the set of all binary trees. We will show that the number of leaves in a full binary tree is one more than the number of interior nodes. Suppose there is a counterexample; then there must exist one with the minimal possible number of interior nodes. This counterexample, C, has n interior nodes and l leaves, where n+1 ≠ l. Moreover, C must be nontrivial, because the trivial tree has n = 0 and l = 1 and is therefore not a counterexample. C therefore has at least one leaf whose parent node is an interior node. Delete this leaf and its parent from the tree, promoting the leaf's sibling node to the position formerly occupied by its parent. This reduces both n and l by 1, so the new tree also has n+1 ≠ l and is therefore a smaller counterexample. But by hypothesis, C was already the smallest counterexample; therefore, the supposition that there were any counterexamples to begin with must have been false. The partial ordering implied by 'smaller' here is the one that says that S < T whenever S has fewer nodes than T.
Structural recursion
Structural recursion bears the same relationship to structural induction as ordinary recursion bears to ordinary mathematical induction.de:Strukturelle Induktion es:Inducción estructural pl:Indukcja strukturalna zh:结构归纳法