Основы функционального программирования/Доказательство свойств функций

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

,

где — рассматриваемое свойство. Например:

Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, то есть справедливые для всей области .

Далее рассматриваются некоторые виды областей определения .

1. линейно упорядоченное множество.

Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, то есть:

.

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

Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. То есть достаточно доказать два пункта:

  1. — базис индукции;
  2. — шаг индукции.

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

2. — определяется как индуктивный класс

Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант , либо набор первичных типов . Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы , определённые над и , и справедливо, что:

.

В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:

  1. необходимо доказать для базиса класса;
  2. Шаг индукции: .

Например, для доказательства свойств функций для списков (тип ), достаточно доказать рассматриваемое свойство для двух следующих случаев:

  1. .
  2. .

Доказательство свойств функций над -выражениями (тип ) можно проводить на основе следующей индукции:

  1. .
  2. .

Пример 23. Доказать, что .

Для доказательства этого свойства можно использовать только определение типа и самой функции (в инфиксной записи используется символ ).

  1. . Базис индукции доказан.
  2. . Теперь пусть применяется конструктор: . Необходимо доказать, что . Это делается при помощи применения второго клоза определения функции :

.

Пример 24. Доказать ассоциативность функции .

То есть необходимо доказать, что для любых трёх списков , и имеет место равенство . При доказательстве индукция будет проводиться по первому операнду, то есть списку :

  1. :

.

.

  1. Пусть для списков , и ассоциативность функции доказана. Необходимо доказать для , и :

.

.

Как видно, последние два выведенных выражения равны, так как для списков , и ассоциативность полагается доказанной.

Пример 25. Доказательство тождества двух определений функции .

Определение 1:

Определение 2:

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

.

1. Базис — :

.

.

2. Шаг — пусть для списка тождество функций и доказано. Необходимо доказать его для списка .

.

.

Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом . Это также делается по индукции:

2.1. Базис — :

.

.

2.2. Шаг — :

.

.

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

Индукционная гипотеза: . Эта индукционная гипотеза является обобщением выражения .

Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 2.2 выглядит следующим образом:

.

.

Что и требовалось доказать.

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