http://wiki.karljones.com/index.php?action=history&feed=atom&title=Structural_induction 2026-10-24T00:42:08Z Revision history for this page on the wiki MediaWiki 1.24.2 http://wiki.karljones.com/index.php?title=Structural_induction&diff=18398&oldid=prev 2016-09-15T20:19:05Z

<p>Created page with &quot;In <a href="/index.php/Mathematical_logic" title="Mathematical logic">mathematical logic</a>, &#039;&#039;&#039;structural induction&#039;&#039;&#039; is a proof method that is used in <a href="/index.php/Computer_science" title="Computer science">computer science</a>, <a href="/index.php/Graph_theory" title="Graph theory">graph theory</a>, and some other mathematical fields. == Descrip...&quot;</p> <p><b>New page</b></p><div>In [[mathematical logic]], '''structural induction''' is a proof method that is used in [[computer science]], [[graph theory]], and some other mathematical fields.<br /> <br /> == Description ==<br /> <br /> It is a generalization of mathematical induction over [[Natural number|natural numbers]], and can be further generalized to arbitrary Noetherian induction.<br /> <br /> Structural recursion is a [[Recursion (computer science)|recursion]] method bearing the same relationship to structural induction as ordinary recursion bears to ordinary [[mathematical induction]].<br /> <br /> Structural induction is used to prove that some proposition P(x) holds for all x of some sort of recursively defined structure such as lists or trees.<br /> <br /> A well-founded partial order is defined on the structures (&quot;sublist&quot; for lists and &quot;subtree&quot; 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.)<br /> <br /> A structurally recursive function uses the same idea to define a recursive function: &quot;base cases&quot; 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.<br /> <br /> For example, if the structures are lists, one usually introduces the partial order '&lt;' in which L &lt; 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.<br /> <br /> 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.<br /> <br /> == See also ==<br /> <br /> * [[Coinduction]]<br /> * [[Initial algebra]]<br /> * [[Loop invariant]], analog for loops<br /> * [[Mathematical logic]]<br /> * [[Recursion (computer science)]]<br /> <br /> == External links ==<br /> <br /> * [https://en.wikipedia.org/wiki/Structural_induction Structural induction] @ Wikipedia.org <br /> <br /> [[Category:Computer science]]<br /> [[Category:Logic]]<br /> [[Category:Mathematics]]<br /> [[Category:Recursion]]</div>

Karl Jones