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

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

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

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

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

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

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

Примеры

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

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

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

В простейшем случае дерево показывает только одного человека и, следовательно, одно поколение; свойство справедливо для такого дерева, поскольку $1 \leq 2 1 - 1$ .
Альтернативно, на дереве изображены один человек и деревья его родителей. Поскольку каждый из последних является подструктурой всего дерева, можно предположить, что он удовлетворяет доказываемому свойству (так называемому гипотезе индукции ). То есть p ≤ 2 ^г − 1 и q ≤ 2 ^час 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. г + 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$ оказывается пустым списком $[]$ . Рассмотрим $эквалайзер$ :

{\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}}

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

Упорядоченный

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

В качестве примера аргумента этого типа рассмотрим набор всех двоичных деревьев . Мы покажем, что количество листьев в полном бинарном дереве на один больше, чем количество внутренних узлов. Предположим, существует контрпример; тогда должен существовать такой, у которого минимально возможное число внутренних узлов. Этот контрпример $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-е изд.). Чтение мессы: Аддисон-Уэсли. ISBN 978-0-201-44124-6 .
«Математическая логика - Видео 01.08 - Обобщенная (структурная) индукция» на YouTube

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

Берстолл, РМ (1969). «Доказательство свойств программ методом структурной индукции». Компьютерный журнал . 12 (1): 41–48. дои : 10.1093/comjnl/12.1.41 .
Обен, Раймонд (1976), Механизация структурной индукции , EDI-INF-PHD, vol. 76–002, Эдинбургский университет, hdl : 1842/6649
Хют, Г.; Халлот, Дж. М. (1980). «Доказательства по индукции в уравнениях с конструкторами» (PDF) . 21-я Анна. Симп. по основам информатики . IEEE. стр. 96–107.
Рожа Петер , Об обобщении теории рекурсивных функций для абстрактных величин с подходящими структурами в качестве областей , Международный симпозиум, Варшава, сентябрь (1959) ( Об обобщении теории рекурсивных функций для абстрактных величин с подходящими структурами в качестве областей ) .