Введение
Метод доказательства в математической логике
Структурная индукция — это метод доказательства, используемый в математической логике (например, при доказательстве теоремы Лоша), информатике, теории графов и некоторых других математических областях. Это обобщение математической индукции для натуральных чисел, которое может быть далее обобщено до произвольной индукции Ноэтера. Структурная рекурсия — это метод рекурсии, который относится к структурной индукции так же, как обычная рекурсия относится к обычной математической индукции. Структурная индукция используется для доказательства того, что некоторое утверждение P(x) верно для всех x некоторой рекурсивно определённой структуры, такой как формулы, списки или деревья. На структурах определяется хорошо обоснованный частичный порядок («подформула» для формул, «подсписок» для списков и «поддерево» для деревьев). Структурное индукционное доказательство представляет собой доказательство того, что утверждение верно для всех минимальных структур и что, если оно верно для непосредственных подструктур некоторой структуры S, то оно должно быть верно и для S. (Формально говоря, это удовлетворяет предпосылкам аксиомы хорошо обоснованной индукции, которая утверждает, что этих двух условий достаточно для истинности утверждения для всех x.) Структурно рекурсивная функция использует ту же идею для определения рекурсивной функции: «базовые случаи» обрабатывают каждую минимальную структуру, а правило определяет рекурсию. Правильность структурной рекурсии обычно доказывается структурной индукцией; в особенно простых случаях индуктивный шаг часто опускается. Функции length и ++ в приведённом ниже примере являются структурно рекурсивными. Например, если структуры — это списки, обычно вводится частичный порядок "<", в котором L < M, если список L является хвостом списка M. При этом упорядочении пустой список [] является единственным минимальным элементом. Структурное индукционное доказательство некоторого утверждения P(L) состоит из двух частей: доказательство того, что P([]) верно, и доказательство того, что если P(L) верно для некоторого списка L и L является хвостом списка M, то P(M) также должно быть верно. В зависимости от того, как была построена функция или структура, может существовать более одного базового случая и/или более одного индуктивного случая. В этих случаях структурное индукционное доказательство некоторого утверждения P(L) состоит из:
formulas, lists, or trees. A well founded partial order 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 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:
Хороший порядок
Так же, как стандартная математическая индукция эквивалентна принципу хорошего упорядочения, структурная индукция также эквивалентна принципу хорошего упорядочения. Если множество всех структур определенного типа допускает хорошо обоснованный частичный порядок, то каждое непустое подмножество должно иметь минимальный элемент. (Это определение "хорошо обоснованности".) Значение леммы в этом контексте заключается в том, что она позволяет нам заключить, что если существуют какие-либо контрпримеры к теореме, которую мы хотим доказать, то должен существовать минимальный контрпример. Если мы можем показать, что существование минимального контрпримера влечет за собой существование еще меньшего контрпримера, мы получим противоречие (поскольку минимальный контрпример не является минимальным), и, следовательно, множество контрпримеров должно быть пустым. В качестве примера такого рода рассуждений рассмотрим множество всех двоичных деревьев. Мы покажем, что количество листьев в полном двоичном дереве на один больше, чем количество внутренних узлов. Предположим, что существует контрпример; тогда должен существовать контрпример с минимальным возможным количеством внутренних узлов. Этот контрпример, C, имеет n внутренних узлов и l листьев, где l = n + 1 ≠ l. Кроме того, C должен быть нетривиальным, потому что тривиальное дерево имеет l = n = 0 и l = 1, и, следовательно, не является контрпримером. Следовательно, C имеет по крайней мере один лист, родительский узел которого является внутренним узлом. Удалите этот лист и его родительский узел из дерева, переместив брата (или сестру) листа на позицию, ранее занимаемую его родителем. Это уменьшает и n, и l на 1, поэтому новое дерево также имеет l = n + 1 ≠ l и, следовательно, является меньшим контрпримером. Но по предположению, C уже был наименьшим контрпримером; следовательно, предположение о том, что изначально существовали какие-либо контрпримеры, должно быть ложным. Частичный порядок, подразумеваемый здесь понятием "меньше", означает, что S < T, когда S имеет меньше узлов, чем T.