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

Материал из Викиучебника

< Основы функционального программирования

Вводная лекция
Структуры данных и базисные операции:
- Первая часть
- Вторая часть

Основы языка Haskell

Конструирование функций
Доказательство свойств функций
Формализация функционального программирования на основе λ-исчисления
Трансформация программ

Категория «Функциональное программирование» →

Формальная задача: пусть имеется набор функций $f = \langle f_1,\, \ldots,\, f_n \rangle$ , определённых на областях $D = \langle D_1,\, \ldots,\, D_n \rangle$ . Требуется доказать, что для любого набора значений $d$ имеет место некоторое свойство, то есть:

$\forall\, d \in D : P\Big(f(d)\Big)$ ,

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

$\forall\, d \in D : f(d) \geqslant 0$

$\forall\, d \in D : f(d) = f\Big(f(d)\Big)$

$\forall\, d \in D : f(d) = f_1(d)$

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

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

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

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

$\forall\, d_1, d_2 \in D : (d_1 \geqslant d_2) \lor (d_1 \leqslant d_2)$ .

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

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

$P\Big(f(\varnothing)\Big)$ — базис индукции;
$\forall\, d_1, d_2 \in D,\ d_1 \leqslant d_2 : P\Big(f(d_1)\Big)$ — шаг индукции.

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

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

Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант $d_i = 0, n \in D$ , либо набор первичных типов $A_i = 0, n : d \in A_i \Rightarrow d \in D$ . Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы $g_1, \ldots, g_m$ , определённые над $A i$ и $D$ , и справедливо, что:

$(a_i \in A_i) \land (x_j \in D) \Rightarrow g_k(a_i, x_j) \in D,\ k = \overline{1, m}$ .

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

$P\Big(f(d)\Big)$ необходимо доказать для базиса класса;
Шаг индукции: $P\Big(f(d)\Big) = P\bigg(f\Big(g_i(d)\Big)\bigg)$ .

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

$P\Big(f([\,])\Big)$ .
$\forall\, a \in D,\, \forall\,L \in \operatorname{List}(A) : P\Big(f(L)\Big) \Rightarrow P\Big(f(a : L)\Big)$ .

Доказательство свойств функций над $S$ -выражениями (тип $\operatorname{S-expr}(A)$ ) можно проводить на основе следующей индукции:

$\forall\, a \in A : P\Big(f(a)\Big)$ .
$\forall\, x, y \in \operatorname{S-expr}(A) : P\Big(f(x)\Big) \land P\Big(f(y)\Big) \Rightarrow P\Big(f(x : y)\Big)$ .

Пример 23. Доказать, что $\forall\, L \in \operatorname{List}(A) : L * [\,] = L$ .

Для доказательства этого свойства можно использовать только определение типа $\operatorname{List}(A)$ и самой функции $\operatorname{append}$ (в инфиксной записи используется символ $*$ ).

$L = [\,] : [\,] * [\,] = [\,] = L$ . Базис индукции доказан.
$\forall\, L \in \operatorname{List}(A) : L * [\,] = L$ . Теперь пусть применяется конструктор: $a : L$ . Необходимо доказать, что $(a : L) * [\,] = a : L$ . Это делается при помощи применения второго клоза определения функции $\operatorname{append}$ :

$(a : L) * [\,] = a : (L * [\,]) = a : (L) = a : L$ .

Пример 24. Доказать ассоциативность функции $\operatorname{append}$ .

То есть необходимо доказать, что для любых трёх списков $L 1$ , $L 2$ и $L 3$ имеет место равенство $(L 1 * L 2) * L 3 = L 1 * (L 2 * L 3)$ . При доказательстве индукция будет проводиться по первому операнду, то есть списку $L 1$ :

$L_1 = [\,]$ :

$([\,] * L_2) * L_3 = (L_2) * L_3 = L_2 * L_3$ .

$[\,] * (L_2 * L_3) = (L_2 * L_3) = L_2 * L_3$ .

Пусть для списков $L 1$ , $L 2$ и $L 3$ ассоциативность функции $\operatorname{append}$ доказана. Необходимо доказать для $(a : L 1)$ , $L 2$ и $L 3$ :

$\Big((a : L_1) * L_2\Big) * L_3 = \Big(a : (L_1 * L_2)\Big) * L_3 = a : \Big((L_1 * L_2) * L_3\Big)$ .

$(a : L_1) * (L_2 * L_3) = a : \Big(L_1 * (L_2 * L_3)\Big)$ .

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

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

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

$\operatorname{reverse}\ [\,] = [\,]$

$\operatorname{reverse}\ (H : T) = (\operatorname{reverse}\ T) * [H]$

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

$\operatorname{reverse}'\; L = \operatorname{rev}\ L [\,]$

$\operatorname{rev}\ [\,]\ L = L$

$\operatorname{rev}\ (H : T)\ L = \operatorname{rev}\ T\ (H : L)$

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

$\forall\, L \in \operatorname{List}(A) : \operatorname{reverse}\ L = \operatorname{reverse}'\; L$ .

1. Базис — $L = [\,]$ :

$\operatorname{reverse}\ [\,] = [\,]$ .

$\operatorname{reverse}'\; [\,] = \operatorname{rev}\ [\,]\ [\,] = [\,]$ .

2. Шаг — пусть для списка $L$ тождество функций $\operatorname{reverse}$ и $\operatorname{reverse}'$ доказано. Необходимо доказать его для списка $(H : L)$ .

$\operatorname{reverse}\ (H : L) = (\operatorname{reverse}\ L) * [H] = (\operatorname{reverse}'\; L) * [H]$ .

$\operatorname{reverse}'\; (H : L) = \operatorname{rev}\ (H : L)\ [\,] = \operatorname{rev}\ L\ (H : [\,]) = \operatorname{rev}\ L\ [H]$ .

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

2.1. Базис — $L = [\,]$ :

$(\operatorname{reverse}'\; [\,]) * [H] = (\operatorname{rev}\ [\,]\; [\,]) * [H] = [\,] * [H] = [H]$ .

$\operatorname{rev}\ [\,]\ [H] = [H]$ .

2.2. Шаг — $L = (A : T)$ :

$\Big(\operatorname{reverse}'\; (A : T)\Big) * [H] = \Big(\operatorname{rev}\ (A : T)\ [\,]\Big) * [H] = \Big(\operatorname{rev}\ T\ (A : [\,])\Big) * [H] = (\operatorname{rev}\ T\ [A]) * [H]$ .

$\operatorname{rev}\ (A : T)\ [H] = \operatorname{rev}\ L\ (A : H)$ .

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

Индукционная гипотеза: $(\operatorname{reverse}'\; L_1) * L_2 = \operatorname{rev}\ L_1\ L_2$ . Эта индукционная гипотеза является обобщением выражения $(\operatorname{reverse}'\; L) * [H] = \operatorname{rev}\ L\ [H]$ .

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

$\Big(\operatorname{reverse}'\; (A : T)\Big) * L_2 = (\operatorname{rev}\ (A : T)\ [\,]) * L_2 = (\operatorname{rev}\ T\ [A]) * L_2 =$

$= \Big((\operatorname{reverse}'\; T) * [A]\Big) * L_2 = (\operatorname{reverse}'\; T) * ([A] * L_2) = (\operatorname{reverse}'\; T) * (A : L_2)$ .

$\operatorname{rev}\ (A : T)\ L_2 = \operatorname{rev}\ T\ (A : L_2) = (\operatorname{reverse}'\; T) * (A : L_2)$ .

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

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

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

Материал из Викиучебника

Просмотры

Личные инструменты

Навигация

участие

Поиск

Инструменты

Печать/Экспорт