Шаг 4.
Основы языка Haskell. Индуктивные определения операций и предикатов, заданных на множествах слов. Принцип трансфинитной индукции

    На этом шаге мы рассмотрим суть этого принципа.

    Метод математической индукции применяется для доказательства утверждений о индуктивно заданных множествах. При этом способ индуктивного задания множества подсказывает, какой разновидностью математической индукции можно воспользоваться.

    Ответим вначале на следующий естественный вопрос: для каких частично упорядоченных множеств имеет место утверждение, аналогичное принципу полной математической индукции?

Определение (по [1]).
Трансфинитная индукция - это способ математических доказательств (называемый принципом трансфинитной индукции), обобщающий принцип математической индукции на произвольные вполне упорядоченные множества.

    Фактически для доказательства правильности индуктивных определений всегда применяется трансфинитная индукция (либо ее частные случаи: натуральная или полная индукция).

Теорема (принцип трансфинитной индукции).
(1) Пусть S(x) - некоторое высказывание об элементе x ∈ Х, Х - вполне упорядоченное множество, и доказаны следующие утверждения:
  1. S(x0), где x0 - наименьший элемент в Х;
  2. для всех x ∈ Х, для которых x>x0, если справедливо S(y) для всех у<х, то справедливо и S(x).
Тогда имеет место S(x) для всех x ∈ Х.

(2) [1, с.586] Если некоторое предположение верно для первого элемента вполне упорядоченного множества X и если из того, что оно верно для всех элементов множества X, предшествующих данному элементу x из множества X, следует его справедливость и для элемента x, то это предположение верно для каждого элемента множества X.


Примеры трансфинитной индукции (по [1]).
  1. Полная индукция на множестве  N.
  2. Индукция по параметру, который пробегает множество всех слов в данном алфавите, упорядоченных лексикографически.
  3. Индукция по построению формул в логико-математическом языке.

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


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

(1)Математический энциклопедический словарь. - М.: Сов. энциклопедия, 1995. - 847 с.

    На следующем шаге мы рассмотрим язык структурированных программ.




Предыдущий шаг Содержание Следующий шаг