Формальная задача: пусть имеется набор функций
, определённых на областях
. Требуется доказать, что для любого набора значений
имеет место некоторое свойство, то есть:
,
где
— рассматриваемое свойство. Например:
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, то есть справедливые для всей области
.
Далее рассматриваются некоторые виды областей определения
.
1.
— линейно упорядоченное множество.
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, то есть:
.
В качестве примера можно привести множество целых чисел. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить отношение порядка.
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. То есть достаточно доказать два пункта:
— базис индукции;
— шаг индукции.
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа
.
2.
— определяется как индуктивный класс
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант
, либо набор первичных типов
. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы
, определённые над
и
, и справедливо, что:
.
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:
необходимо доказать для базиса класса;
- Шаг индукции:
.
Например, для доказательства свойств функций для списков (тип
), достаточно доказать рассматриваемое свойство для двух следующих случаев:
.
.
Доказательство свойств функций над
-выражениями (тип
) можно проводить на основе следующей индукции:
.
.
Пример 23. Доказать, что
.
Для доказательства этого свойства можно использовать только определение типа
и самой функции
(в инфиксной записи используется символ
).
. Базис индукции доказан.
. Теперь пусть применяется конструктор:
. Необходимо доказать, что
. Это делается при помощи применения второго клоза определения функции
:
.
Пример 24. Доказать ассоциативность функции
.
То есть необходимо доказать, что для любых трёх списков
,
и
имеет место равенство
. При доказательстве индукция будет проводиться по первому операнду, то есть списку
:
:
.
.
- Пусть для списков
,
и
ассоциативность функции
доказана. Необходимо доказать для
,
и
:
.
.
Как видно, последние два выведенных выражения равны, так как для списков
,
и
ассоциативность полагается доказанной.
Пример 25. Доказательство тождества двух определений функции
.
Определение 1:
Определение 2:
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что:
.
1. Базис —
:
.
.
2. Шаг — пусть для списка
тождество функций
и
доказано. Необходимо доказать его для списка
.
.
.
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом
. Это также делается по индукции:
2.1. Базис —
:
.
.
2.2. Шаг —
:
.
.
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут всё усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.
Индукционная гипотеза:
. Эта индукционная гипотеза является обобщением выражения
.
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 2.2 выглядит следующим образом:
.
.
Что и требовалось доказать.
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.