Структурная индукция - Structural induction

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

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

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

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

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

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

Примеры

Древнее древо предков, на котором изображен 31 человек в 5 поколениях

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

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

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

  • В простейшем случае дерево показывает только одного человека и, следовательно, одно поколение; свойство верно для такого дерева, так как 1 ≤ 21 − 1.
  • Как вариант, дерево показывает одного человека и деревья его родителей. Поскольку каждая из последних является подструктурой всего дерева, можно предположить, что она удовлетворяет доказываемому свойству (также известному как гипотеза индукции). Это, п ≤ 2грамм − 1 и q ≤ 2час − 1 можно предположить, где грамм и час обозначает количество поколений, на которые распространяется поддерево отца и матери, соответственно, и п и q обозначают количество людей, которых они показывают.
    • В случае грамм ≤ час, все дерево простирается на 1 + час поколения и шоу п + q + 1 человек, и п + q + 1 ≤ (2грамм − 1) + (2час − 1) + 1 ≤ 2час + 2час − 1 = 21+час − 1, т.е. все дерево удовлетворяет свойству.
    • В случае час ≤ грамм, все дерево простирается на 1 + грамм поколения и шоу п + q + 1 ≤ 21 + грамм − 1 людей по аналогичным рассуждениям, т.е. все дерево удовлетворяет свойству и в этом случае.

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

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

    длина (L ++ M) = длина L + длина M [EQ]

Здесь ++ обозначает операцию конкатенации списков, а L и M - списки.

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

    длина [] = 0 [LEN1] длина (h: t) = 1 + длина t [LEN2]
    [] ++ список = список [APP1] (h: t) ++ list = h: (t ++ список) [APP2]

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

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

      длина (L ++ M) = длина ([] ++ M) = длина M (по APP1) = 0 + длина M = длина [] + длина M (по LEN1) = длина L + длина M

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

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

    длина (xs ++ M) = длина xs + длина M (гипотеза)

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

    длина L + длина M = длина (x: xs) + длина M = 1 + длина xs + длина M (по LEN2) = 1 + длина (xs ++ M) (по гипотезе) = длина (x: (xs ++ M)) (по LEN2) = длина ((x: xs) ++ M) (по APP2) = длина (L ++ M)

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

Хороший порядок

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

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

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

Рекомендации

  • Хопкрофт, Джон Э .; Раджив Мотвани; Джеффри Д. Ульман (2001). Введение в теорию автоматов, языки и вычисления (2-е изд.). Месса для чтения: Эддисон-Уэсли. ISBN  978-0-201-44124-6.

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