Структурная индукция

Структурная индукция — метод доказательства , который используется в математической логике (например, в доказательстве теоремы Лося ), информатике , теории графов и некоторых других областях математики. Это обобщение математической индукции по натуральным числам , которое может быть далее обобщено до произвольной нётеровой индукции . Структурная рекурсия — метод рекурсии, имеющий такое же отношение к структурной индукции, как обычная рекурсия имеет к обычной математической индукции .

Структурная индукция используется для доказательства того, что некоторое предложение $P (x)$ справедливо для всех $x$ некоторого вида рекурсивно определенной структуры, такой как формулы , списки или деревья . На структурах определяется обоснованный частичный порядок («подформула» для формул, «подсписок» для списков и «поддерево» для деревьев). Доказательство структурной индукции — это доказательство того, что предложение справедливо для всех минимальных структур и что если оно справедливо для непосредственных подструктур определенной структуры $S$ , то оно должно справедливо и для $S$ . (Формально говоря, это удовлетворяет предпосылкам аксиомы обоснованной индукции , которая утверждает, что эти два условия достаточны для того, чтобы предложение справедливо для всех $x$ .)

Структурно рекурсивная функция использует ту же идею для определения рекурсивной функции: «базовые случаи» обрабатывают каждую минимальную структуру и правило для рекурсии. Структурная рекурсия обычно доказывается корректной структурной индукцией; в особенно простых случаях индуктивный шаг часто опускается. Функции length и ++ в примере ниже являются структурно рекурсивными.

Например, если структуры являются списками, обычно вводят частичный порядок "<", в котором $L < M$ всякий раз, когда список $L$ является хвостом списка $M$ . При таком порядке пустой список $[]$ является единственным минимальным элементом. Доказательство структурной индукции некоторого предложения $P (L)$ тогда состоит из двух частей: доказательства того, что $P ([])$ истинно, и доказательства того, что если $P (L)$ истинно для некоторого списка $L$ , и если $L$ является хвостом списка $M$ , то $P (M)$ также должно быть истинным.

В конце концов, может существовать более одного базового случая и/или более одного индуктивного случая, в зависимости от того, как была построена функция или структура. В этих случаях доказательство структурной индукции некоторого предложения $P (L)$ состоит из:

доказательство того, что $P (BC)$ верно для каждого базового случая $BC$ ,
доказательство того, что если $P (I)$ истинно для некоторого экземпляра $I$ и $M$ может быть получено из $I$ путем применения любого одного рекурсивного правила один раз, то $P (M)$ также должно быть истинным.

Примеры

Древо предков — это общеизвестная структура данных, показывающая родителей, бабушек и дедушек и т. д. человека, насколько это известно (см. рисунок для примера). Оно рекурсивно определяется:

В простейшем случае генеалогическое древо показывает только одного человека (если о его родителях ничего не известно);
В качестве альтернативы, дерево предков показывает одного человека и, соединенные ветвями, два поддерева предков его родителей (используя для краткости доказательства упрощающее предположение, что если известен один из них, известны и оба).

Например, свойство «Предковое дерево, простирающееся на $g$ поколений, показывает не более $2 g - 1$ человек» можно доказать с помощью структурной индукции следующим образом:

В простейшем случае дерево показывает только одного человека и, следовательно, одно поколение; свойство верно для такого дерева, поскольку $1 \leq 2 1 - 1$ .
В качестве альтернативы дерево показывает одного человека и деревья его родителей. Поскольку каждое из последних является подструктурой всего дерева, можно предположить, что оно удовлетворяет доказываемому свойству (также известному как гипотеза индукции ). То есть, можно предположить , что p ≤ 2 ^g − 1 и q ≤ 2 ^h − 1 , где g и h обозначают количество поколений, на которые простирается поддерево отца и матери соответственно, а p и q обозначают количество людей, которых они показывают.
- В случае $g \leq h$ все дерево простирается на $1 + h$ поколений и показывает $p + q + 1$ человек, т. е. все дерево удовлетворяет свойству. $p+q+1\leq (2^{g}-1)+(2^{h}-1)+1\leq 2^{h}+2^{h}-1=2^{1+h}-1,$
- В случае $h \leq g$ все дерево простирается на $1 + g$ поколений и показывает $p + q + 1 \leq 2 g + 1 - 1$ человек по аналогичным рассуждениям, т.е. все дерево удовлетворяет свойству и в этом случае.

Следовательно, по структурной индукции каждое дерево предков удовлетворяет этому свойству.

В качестве другого, более формального примера рассмотрим следующее свойство списков:

{\text{EQ:}}\quad \operatorname {len} (L+\!+\ M)=\operatorname {len} (L)+\operatorname {len} (M)

Здесь $++$ обозначает операцию конкатенации списков, $len()$ — длину списка, а $L$ и $M$ — списки.

Чтобы доказать это, нам нужны определения длины и операции конкатенации. Пусть $(h : t)$ обозначает список, голова (первый элемент) которого — $h$ , а хвост (список оставшихся элементов) — $t$ , и пусть $[]$ обозначает пустой список. Определения длины и операции конкатенации следующие:

{\begin{array}{ll}{\text{LEN1:}}&\operatorname {len} ([\ ])=0\\{\text{LEN2:}}&\operatorname {len} (h:t)=1+\operatorname {len} (t)\\&\\{\text{APP1:}}&[\ ]+\!+\ list=list\\{\text{APP2:}}&(h:t)+\!+\ list=h:(t+\!+\ list)\end{array}}

Наше предложение $P (l)$ заключается в том, что $EQ$ истинно для всех списков $M,$ когда $L$ равно $l$ . Мы хотим показать, что $P (l)$ истинно для всех списков $l$ . Мы докажем это с помощью структурной индукции по спискам.

Сначала мы докажем, что $P ([])$ истинно; то есть $EQ$ истинно для всех списков $M$ , когда $L$ оказывается пустым списком $[]$ . Рассмотрим $EQ$ :

{\begin{array}{rll}\operatorname {len} (L+\!+\ M)&=\operatorname {len} ([\ ]+\!+\ M)\\&=\operatorname {len} (M)&({\text{by APP1}})\\&=0+\operatorname {len} (M)\\&=\operatorname {len} ([\ ])+\operatorname {len} (M)&({\text{by LEN1}})\\&=\operatorname {len} (L)+\operatorname {len} (M)\\\end{array}}

Итак, эта часть теоремы доказана; $уравнение EQ$ верно для всех $M$ , когда $L$ равно $[]$ , поскольку левая и правая части равны.

Далее рассмотрим любой непустой список $I$ . Поскольку $I$ непустой, у него есть головной элемент $x$ и хвостовой список $xs$ , поэтому мы можем выразить его как $(x : xs)$ . Гипотеза индукции заключается в том, что $EQ$ истинно для всех значений $M,$ когда $L$ равно $xs$ :

{\text{HYP:}}\quad \operatorname {len} (xs+\!+\ M)=\operatorname {len} (xs)+\operatorname {len} (M)

Мы хотели бы показать, что если это так, то $EQ$ также верно для всех значений $M$ , когда $L = I = (x : xs)$ . Продолжаем, как и прежде:

{\begin{array}{rll}\operatorname {len} (L)+\operatorname {len} (M)&=\operatorname {len} (x:xs)+\operatorname {len} (M)\\&=1+\operatorname {len} (xs)+\operatorname {len} (M)&({\text{by LEN2}})\\&=1+\operatorname {len} (xs+\!+\ M)&({\text{by HYP}})\\&=\operatorname {len} (x:(xs+\!+\ M))&({\text{by LEN2}})\\&=\operatorname {len} ((x:xs)+\!+\ M)&({\text{by APP2}})\\&=\operatorname {len} (L+\!+\ M)\end{array}}

Таким образом, из структурной индукции получаем, что $P (L)$ истинно для всех списков $L$ .

Хорошо упорядоченный

Так же, как стандартная математическая индукция эквивалентна принципу хорошо упорядоченного порядка , структурная индукция также эквивалентна принципу хорошо упорядоченного порядка. Если множество всех структур определенного вида допускает хорошо обоснованный частичный порядок, то каждое непустое подмножество должно иметь минимальный элемент. (Это определение « хорошо обоснованного ».) Значение леммы в этом контексте заключается в том, что она позволяет нам вывести, что если есть какие-либо контрпримеры к теореме, которую мы хотим доказать, то должен быть минимальный контрпример. Если мы можем показать, что существование минимального контрпримера влечет еще меньший контрпример, мы получаем противоречие (поскольку минимальный контрпример не является минимальным), и поэтому множество контрпримеров должно быть пустым.

В качестве примера такого типа аргумента рассмотрим множество всех бинарных деревьев . Мы покажем, что количество листьев в полном бинарном дереве на один больше, чем количество внутренних узлов. Предположим, что есть контрпример; тогда должен существовать один с минимально возможным количеством внутренних узлов. Этот контрпример, $C$ , имеет $n$ внутренних узлов и $l$ листьев, где $n + 1 \neq l$ . Более того, $C$ должен быть нетривиальным, потому что тривиальное дерево имеет $n = 0$ и $l = 1$ и, следовательно, не является контрпримером. Следовательно, $C$ имеет по крайней мере один лист, родительский узел которого является внутренним узлом. Удалим этот лист и его родителя из дерева, продвигая родственный узел листа на позицию, ранее занимаемую его родителем. Это уменьшает как $n$ , так и $l$ на 1, поэтому новое дерево также имеет $n + 1 \neq l$ и, следовательно, является меньшим контрпримером. Но по гипотезе $C$ уже был наименьшим контрпримером; следовательно, предположение о том, что изначально были какие-либо контрпримеры, должно быть ложным. Частичный порядок, подразумеваемый здесь под «меньше», — это тот, который говорит, что S $< T всякий$ раз, когда $S$ имеет меньше узлов, чем $T.$

Смотрите также

Ссылки

Хопкрофт, Джон Э.; Раджив Мотвани; Джеффри Д. Ульман (2001). Введение в теорию автоматов, языки и вычисления (2-е изд.). Массовое чтение: Addison-Wesley. ISBN 978-0-201-44124-6.
«Математическая логика - Видео 01.08 - Обобщенная (структурная) индукция» на YouTube

Ранние публикации о структурной индукции включают:

Берстолл, Р. М. (1969). «Доказательство свойств программ с помощью структурной индукции». The Computer Journal . 12 (1): 41–48. doi :10.1093/comjnl/12.1.41.
Обин, Рэймонд (1976), Механизация структурной индукции , EDI-INF-PHD, т. 76–002, Эдинбургский университет, hdl :1842/6649
Хью, Г.; Халлот, Дж. М. (1980). «Доказательства индукцией в эквациональных теориях с конструкторами» (PDF) . 21-й ежегодный симпозиум по основам компьютерной науки . IEEE. стр. 96–107.
Рожа Петер , Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche , Международный симпозиум, Варшава, сентябрь (1959 г.) ( Об обобщении теории рекурсивных функций для абстрактных величин с подходящими структурами в качестве областей определения ) .