HOME

TheInfoList



OR:

Structural induction is a proof method that is used in
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
(e.g., in the proof of Łoś' theorem),
computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
,
graph theory In mathematics and computer science, graph theory is the study of ''graph (discrete mathematics), graphs'', which are mathematical structures used to model pairwise relations between objects. A graph in this context is made up of ''Vertex (graph ...
, and some other mathematical fields. It is a generalization of mathematical induction over natural numbers and can be further generalized to arbitrary Noetherian induction. Structural recursion is a
recursion Recursion occurs when the definition of a concept or process depends on a simpler or previous version of itself. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in m ...
method bearing the same relationship to structural induction as ordinary recursion bears to ordinary
mathematical induction Mathematical induction is a method for mathematical proof, proving that a statement P(n) is true for every natural number n, that is, that the infinitely many cases P(0), P(1), P(2), P(3), \dots  all hold. This is done by first proving a ...
. Structural induction is used to prove that some proposition holds
for all In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", "for every", or "given an arbitrary element". It expresses that a predicate can be satisfied by e ...
of some sort of recursively defined structure, such as
formulas In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
, lists, or
trees In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only p ...
. A
well-founded In mathematics, a binary relation is called well-founded (or wellfounded or foundational) on a set (mathematics), set or, more generally, a Class (set theory), class if every non-empty subset has a minimal element with respect to ; that is, t ...
partial order In mathematics, especially order theory, a partial order on a set is an arrangement such that, for certain pairs of elements, one precedes the other. The word ''partial'' is used to indicate that not every pair of elements needs to be comparable ...
is defined on the structures ("subformula" for formulas, "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 , then it must hold for 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 .) 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 whenever list is the tail of list . Under this ordering, the empty list is the unique minimal element. A structural induction proof of some proposition then consists of two parts: A proof that is true and a proof that if is true for some list , and if is the tail of list , then 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 then consists of:


Examples

An ancestor tree is a commonly known data structure, showing the parents, grandparents, etc. of a person as far as known (see picture for an example). It is recursively defined: * in the simplest case, an ancestor tree shows just one person (if nothing is known about their parents); * alternatively, an ancestor tree shows one person and, connected by branches, the two ancestor subtrees of their parents (using for brevity of proof the simplifying assumption that if one of them is known, both are). As an example, the property "An ancestor tree extending over generations shows at most persons" can be proven by structural induction as follows: * In the simplest case, the tree shows just one person and hence one generation; the property is true for such a tree, since . * Alternatively, the tree shows one person and their parents' trees. Since each of the latter is a substructure of the whole tree, it can be assumed to satisfy the property to be proven (a.k.a. the ''induction hypothesis''). That is, and can be assumed, where and denotes the number of generations the father's and the mother's subtree extends over, respectively, and and denote the numbers of persons they show. ** In case , the whole tree extends over generations and shows persons, andp+q+1 \leq (2^g-1) + (2^h-1) + 1 \leq 2^h+2^h-1 = 2^-1,i.e. the whole tree satisfies the property. ** In case , the whole tree extends over generations and shows persons by similar reasoning, i.e. the whole tree satisfies the property in this case also. Hence, by structural induction, each ancestor tree satisfies the property. As another, more formal example, consider the following property of lists : :\text \quad \operatorname(L +\!+\ M) = \operatorname(L) + \operatorname(M) Here denotes the list concatenation operation, the list length, and and are lists. In order to prove this, we need definitions for length and for the concatenation operation. Let denote a list whose head (first element) is and whose tail (list of remaining elements) is , and let denote the empty list. The definitions for length and the concatenation operation are: :\begin \text & \operatorname( = 0 \\ \text & \operatorname(h:t) = 1 + \operatorname(t) \\ & \\ \text & +\!+\ list = list \\ \text & (h:t) +\!+\ list = h : (t +\!+\ list) \end Our proposition is that is true for all lists when is . We want to show that is true for all lists . We will prove this by structural induction on lists. First we will prove that is true; that is, is true for all lists when happens to be the empty list . Consider : :\begin \operatorname(L +\!+\ M) &= \operatorname( +\!+\ M) \\ &= \operatorname(M) & (\text)\\ &= 0 + \operatorname(M) \\ &= \operatorname( + \operatorname(M) & (\text)\\ &= \operatorname(L) + \operatorname(M) \\ \end So this part of the theorem is proved; is true for all , when is , because the left-hand side and the right-hand side are equal. Next, consider any nonempty list . Since is nonempty, it has a head item, , and a tail list, , so we can express it as . The induction hypothesis is that is true for all values of when is : :\text \quad \operatorname(xs +\!+\ M) = \operatorname(xs) + \operatorname(M) We would like to show that if this is the case, then is also true for all values of when . We proceed as before: :\begin \operatorname(L) + \operatorname(M) &= \operatorname(x:xs) + \operatorname(M) \\ &= 1 + \operatorname(xs) + \operatorname(M) & (\text) \\ &= 1 + \operatorname(xs +\!+\ M) & (\text) \\ &= \operatorname(x: (xs +\!+\ M)) & (\text) \\ &= \operatorname((x:xs) +\!+\ M) & (\text) \\ &= \operatorname(L +\!+\ M) \end Thus, from structural induction, we obtain that is true for all lists .


Well-ordering

Just as standard
mathematical induction Mathematical induction is a method for mathematical proof, proving that a statement P(n) is true for every natural number n, that is, that the infinitely many cases P(0), P(1), P(2), P(3), \dots  all hold. This is done by first proving a ...
is equivalent to the
well-ordering principle In mathematics, the well-ordering principle states that every non-empty subset of nonnegative integers contains a least element. In other words, the set of nonnegative integers is well-ordered by its "natural" or "magnitude" order in which x pr ...
, 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 In mathematics, a binary relation is called well-founded (or wellfounded or foundational) on a set (mathematics), set or, more generally, a Class (set theory), class if every non-empty subset has a minimal element with respect to ; that is, t ...
".) 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 In computer science, a binary tree is a tree data structure in which each node has at most two children, referred to as the ''left child'' and the ''right child''. That is, it is a ''k''-ary tree with . A recursive definition using set theor ...
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, , has interior nodes and leaves, where . Moreover, must be nontrivial, because the trivial tree has and and is therefore not a counterexample. 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 and by 1, so the new tree also has and is therefore a smaller counterexample. But by hypothesis, 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 whenever has fewer nodes than .


See also

*
Coinduction In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Coinduction is the mathematical dual to structural induction. Coinductively defined data types are known as coda ...
*
Initial algebra In mathematics, an initial algebra is an initial object in the Category (mathematics), category of F-algebra, -algebras for a given endofunctor . This initiality provides a general framework for mathematical induction, induction and recursion. ...
*
Loop invariant In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked with a code assertion. Knowing its invariant(s) is essential in understanding th ...
, analog for loops


References

* * Early publications about structural induction include: * * * *
Rózsa Péter Rózsa Péter, until January 1934 Rózsa Politzer, (17 February 1905 – 16 February 1977) was a Hungarian mathematician and logician. She is best known as the "founding mother of recursion theory". Early life and education Péter was bor ...
, ''Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche'', Symposium International, Varsovie septembre (1959) (''On the generalization of the theory of recursive functions for abstract quantities with suitable structures as domains''). {{Mathematical logic Graph theory Logic in computer science Mathematical induction Mathematical logic Mathematical proofs Wellfoundedness