Structural induction
Encyclopedia
Structural induction is a proof method that is used in mathematical logic
(e.g., in the proof of Łoś' theorem), computer science
, graph theory
, and some other mathematical fields. It is a generalization of mathematical induction
. Structural recursion is a recursion
method bearing the same relationship to structural induction as ordinary recursion bears to ordinary 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 recursively-defined
structure such as lists or trees. A well-founded partial order is defined on the structures ("sublist" for lists and "subtree" for trees). The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure S, then it must hold for S also. (Formally speaking, this then satisfies the premises of an axiom of well-founded induction, which asserts that these two conditions are sufficient for the proposition to hold for all x.)
A structurally recursive function uses the same idea to define a recursive function: "base cases" handle each minimal structure and a rule for recursion. Structural recursion is usually proved correct by structural induction; in particularly easy cases, the inductive step is often left out. The length and ++ functions in the example below are structurally recursive.
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.
Eventually, there may exist more than one base case, and/or more than one inductive case, depending on how the function or structure was constructed. In those cases, a structural induction proof of some proposition P(l) then consists of: A) a proof that P(BC) is true for each base case BC, and B): a proof that if P(I) is true for some instance I, and M can be obtained from I by applying any one recursive rule once, then P(M) must also be true.
length (L ++ M) = length L + length M [EQ]
Here ++ denotes the list concatenation operation, and L and M are lists.
In order to prove this, we need definitions for length and for the concatenation operation. Let (h:t) denote a list whose head (first element) is h and whose tail (list of remaining elements) is t, and let [] denote the empty list. The definitions for length and the concatenation operation are:
length [] = 0 [LEN1]
length (h:t) = 1 + length t [LEN2]
[] ++ list = list [APP1]
(h:t) ++ list = h : (t ++ list) [APP2]
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 left-hand side and the right-hand 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 are done.
is equivalent to the well-ordering principle
, structural induction is also equivalent to a well-ordering principle. If the set of all structures of a certain kind admits a well-founded partial order, then every nonempty subset must have a minimal element. (This is the definition of "well-founded".) 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 tree
s. 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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
(e.g., in the proof of Łoś' theorem), computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, graph theory
Graph theory
In mathematics and computer science, graph theory is the study of graphs, mathematical structures used to model pairwise relations between objects from a certain collection. A "graph" in this context refers to a collection of vertices or 'nodes' and a collection of edges that connect pairs of...
, and some other mathematical fields. It is a generalization of mathematical induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
. Structural recursion is a recursion
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
method bearing the same relationship to structural induction as ordinary recursion bears to ordinary mathematical induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
.
In general, the idea is that one wishes to prove some proposition P(x), where x is any instance of some sort of recursively-defined
Recursive definition
In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....
structure such as lists or trees. A well-founded partial order is defined on the structures ("sublist" for lists and "subtree" for trees). The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure S, then it must hold for S also. (Formally speaking, this then satisfies the premises of an axiom of well-founded induction, which asserts that these two conditions are sufficient for the proposition to hold for all x.)
A structurally recursive function uses the same idea to define a recursive function: "base cases" handle each minimal structure and a rule for recursion. Structural recursion is usually proved correct by structural induction; in particularly easy cases, the inductive step is often left out. The length and ++ functions in the example below are structurally recursive.
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.
Eventually, there may exist more than one base case, and/or more than one inductive case, depending on how the function or structure was constructed. In those cases, a structural induction proof of some proposition P(l) then consists of: A) a proof that P(BC) is true for each base case BC, and B): a proof that if P(I) is true for some instance I, and M can be obtained from I by applying any one recursive rule once, 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 concatenation operation, and L and M are lists.
In order to prove this, we need definitions for length and for the concatenation operation. Let (h:t) denote a list whose head (first element) is h and whose tail (list of remaining elements) is t, and let [] denote the empty list. The definitions for length and the concatenation operation are:
length [] = 0 [LEN1]
length (h:t) = 1 + length t [LEN2]
[] ++ list = list [APP1]
(h:t) ++ list = h : (t ++ list) [APP2]
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 left-hand side and the right-hand 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 are done.
Well-ordering
Just as standard mathematical inductionMathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
is equivalent to the well-ordering principle
Well-ordering principle
The "well-ordering principle" is a property of ordered sets. A set X is well ordered if every subset of X has a least element. An example of a well ordered set is the set of natural numbers. An example of set that is not well ordered is the set of integers...
, structural induction is also equivalent to a well-ordering principle. If the set of all structures of a certain kind admits a well-founded partial order, then every nonempty subset must have a minimal element. (This is the definition of "well-founded".) 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 tree
Binary tree
In computer science, a binary tree is a tree data structure in which each node has at most two child nodes, usually distinguished as "left" and "right". Nodes with children are parent nodes, and child nodes may contain references to their parents. Outside the tree, there is often a reference to...
s. 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.