Войти
Структурная индукция - это метод доказательства, который используется в математической логике (например, в доказательстве теоремы Лося ), информатике, теории графов и некоторых других областях математики. Это обобщение математической индукции по натуральным числам и может быть далее обобщено для произвольной нётеровой индукции. Структурная рекурсия - это метод рекурсии, имеющий такое же отношение к структурной индукции, как обычная рекурсия к обычной математической индукции.
Структурная индукция используется для доказательства того, что некоторое предложение P ( x ) выполняется для всех x некоторой рекурсивно определенной структуры, такой как формулы, списки или деревья. На структурах определяется хорошо обоснованный частичный порядок («подформула» для формул, «подсписок» для списков и «поддерево» для деревьев). Структурная индукция доказательство является доказательством того, что предложение справедливо для всех минимальных структур и что, если оно имеет место для непосредственных подструктур определенной структуры S, то оно должно быть выполнено для S также. (Формально говоря, тогда это удовлетворяет посылкам аксиомы хорошо обоснованной индукции, утверждающей, что этих двух условий достаточно для выполнения предложения для всех x. )
Структурно рекурсивная функция использует ту же идею для определения рекурсивной функции: «базовые случаи» обрабатывают каждую минимальную структуру и правило рекурсии. Структурная рекурсия обычно подтверждается структурной индукцией; в особенно легких случаях индуктивный шаг часто не учитывается. Функции length и ++ в приведенном ниже примере структурно рекурсивны.
Например, если структуры представляют собой списки, один, как правило, вводит частичный порядок «lt;», в котором L lt; M, когда список L является хвост списка М. При таком порядке пустой список [] является единственным минимальным элементом. Структурное индукционное доказательство некоторого предложения P ( L ) состоит из двух частей: доказательства того, что P ([]) истинно, и доказательства того, что если P ( L ) истинно для некоторого списка L, и если L является хвостом list M, то P ( M ) также должно быть истинным.
В конце концов, может существовать более одного базового случая и / или более одного индуктивного случая, в зависимости от того, как была построена функция или структура. В таких случаях структурное индукционное доказательство некоторого предложения P ( l ) состоит из:
Древнее древо предков, на котором изображен 31 человек в 5 поколениях Предок дерево общеизвестной структура данных, показывая родитель, бабушка и дедушка и т.д. человека, насколько известно (см картинки для примера). Это рекурсивно определяется:
Например, свойство «Древо предков, простирающееся на g поколений, содержит не более 2 г - 1 человека» может быть доказано структурной индукцией следующим образом:
Следовательно, по структурной индукции каждое дерево предков удовлетворяет этому свойству.
В качестве другого, более формального примера рассмотрим следующее свойство списков:
length (L ++ M) = length L + length M [EQ]
Здесь ++ обозначает операцию конкатенации списков, а L и M - списки.
Чтобы доказать это, нам нужны определения длины и операции конкатенации. Пусть (h: t) обозначает список, голова (первый элемент) которого - h, а хвост (список оставшихся элементов) - t, а [] обозначает пустой список. Определения длины и операции конкатенации:
length [] = 0 [LEN1] length (h:t) = 1 + length t [LEN2]
[] ++ list = list [APP1] (h:t) ++ list = h : (t ++ list) [APP2]
Наше предложение P ( l ) состоит в том, что EQ верно для всех списков M, когда L равно l. Мы хотим показать, что P ( l ) истинно для всех списков l. Мы докажем это с помощью структурной индукции по спискам.
Сначала докажем, что P ([]) истинно; то есть EQ истинно для всех списков M, когда L оказывается пустым списком []. Рассмотрим эквалайзер:
length (L ++ M) = length ([] ++ M) = length M (by APP1) = 0 + length M = length [] + length M (by LEN1) = length L + length M
Итак, эта часть теоремы доказана; EQ верно для всех M, когда L равно [], потому что левая и правая части равны.
Далее рассмотрим любой непустой список I. Поскольку I непусто, у него есть заголовок x и конечный список xs, поэтому мы можем выразить его как (x: xs). Гипотеза индукции состоит в том, что EQ верно для всех значений M, когда L равно xs :
length (xs ++ M) = length xs + length M (hypothesis)
Мы хотели бы показать, что если это так, то EQ также верно для всех значений M, когда L = I = (x: xs). Действуем как раньше:
length L + length M = length (x:xs) + length M = 1 + length xs + length M (by LEN2) = 1 + length (xs ++ M) (by hypothesis) = length (x: (xs ++ M)) (by LEN2) = length ((x:xs) ++ M) (by APP2) = length (L ++ M)
Таким образом, из структурной индукции получаем, что P (L) истинно для всех списков L.
Подобно тому, как стандартная математическая индукция эквивалентна принципу хорошего порядка, структурная индукция также эквивалентна принципу хорошего порядка. Если множество всех структур определенного вида допускает хорошо обоснованный частичный порядок, то каждое непустое подмножество должно иметь минимальный элемент. (Это определение « хорошо обоснованного ».) Значение леммы в данном контексте состоит в том, что она позволяет нам сделать вывод, что если есть какие-либо контрпримеры к теореме, которую мы хотим доказать, то должен быть минимальный контрпример. Если мы можем показать, что из существования минимального контрпримера следует еще меньший контрпример, мы получаем противоречие (поскольку минимальный контрпример не минимальный), и поэтому набор контрпримеров должен быть пустым.
В качестве примера этого типа аргумента рассмотрим набор всех двоичных деревьев. Мы покажем, что количество листьев в полном двоичном дереве на единицу больше, чем количество внутренних узлов. Предположим, есть контрпример; тогда должен существовать такой с минимально возможным количеством внутренних узлов. Этот контрпример, C, имеет n внутренних узлов и l листьев, где n + 1 ≠ l. Более того, C должно быть нетривиальным, потому что тривиальное дерево имеет n = 0 и l = 1 и, следовательно, не является контрпримером. Следовательно, C имеет по крайней мере один лист, родительский узел которого является внутренним узлом. Удалите этот лист и его родителя из дерева, переместив родственный узел листа на позицию, ранее занимаемую его родителем. Это уменьшает как n, так и l на 1, так что новое дерево также имеет n + 1 ≠ l и, следовательно, является меньшим контрпримером. Но по гипотезе C уже был наименьшим контрпримером; следовательно, предположение о существовании каких-либо контрпримеров должно было быть ложным. Частичное упорядочение подразумевается «меньше» здесь есть один, который говорит, что S lt; T, когда S имеет меньше узлов, чем Т.
Ранние публикации о структурной индукции включают:
