Основы функционального программирования/Доказательство свойств функций: различия между версиями
Содержимое удалено Содержимое добавлено
мНет описания правки |
Вставлены формулы, взятые с http://roman-dushkin.narod.ru/fp_09.html |
||
Строка 2:
{{ОФП Содержание}}
Формальная задача: пусть имеется набор функций <math>f =
<math>\forall\, d \in D : P\Big(f(d)\Big)</math>,
где <math>P</math> — рассматриваемое свойство. Например:
<math>\forall\, d \in D : f(d) \geqslant 0</math>
<math>\forall\, d \in D : f(d) = f\Big(f(d)\Big)</math>
<math>\forall\, d \in D : f(d) = f_1(d)</math>
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, то есть справедливые для всей области <math>D</math>.
Далее рассматриваются некоторые виды областей определения <math>D</math>.
'''1. <math>D</math> — [[w:Линейно упорядоченное множество|линейно упорядоченное множество]].'''
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, то есть:
<math>\forall\, d_1, d_2 \in D : (d_1 \geqslant d_2) \lor (d_1 \leqslant d_2)</math>.
В качестве примера можно привести [[w:Целое число|множество целых чисел]]. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить [[w:Отношение порядка|отношение порядка]].
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести [[w:Математическая индукция|индукцию]] по данным. То есть достаточно доказать два пункта:
#<math>P\Big(f(\varnothing)\Big)</math> — базис индукции;
#<math>\forall\, d_1, d_2 \in D,\ d_1 \leqslant d_2 : P\Big(f(d_1)\Big)</math> — шаг индукции.
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа <math>D</math>.
'''2. <math>D</math> — определяется как индуктивный класс'''
Из [[Основы функционального программирования/Конструирование функций|прошлой лекции]] известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант <math>d_i = 0, n \in D</math>, либо набор первичных типов <math>A_i = 0, n : d \in A_i \Rightarrow d \in D</math>. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы <math>g_1, \ldots, g_m</math>, определённые над <math>A_i</math> и <math>D</math>, и справедливо, что:
<math>(a_i \in A_i) \land (x_j \in D) \Rightarrow g_k(a_i, x_j) \in D,\ k = \overline{1, m}</math>.
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:
#<math>P
# Шаг индукции: <math>P
Например, для доказательства свойств функций для списков (тип <math>\operatorname{List
# <math>P
# <math>\forall\, a \in D,\, \forall\,L \in \operatorname{List}(A) : P\Big(f(L)\Big) \Rightarrow P\Big(f(a : L)\Big)</math>.
Доказательство свойств функций над <math>S</math>-выражениями (тип <math>\operatorname{S-expr
# <math>\forall\, a \in A : P\Big(f(a)\Big)</math>.
# <math>\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)</math>.
'''Пример 23. Доказать, что <math>\forall\, L \in \operatorname{List}(A) : L * [\,] = L</math>.'''
Для доказательства этого свойства можно использовать только определение типа <math>\operatorname{List
# <math>L = [\,] : [\,] * [\,] = [\,] = L</math>. Базис индукции доказан.
# <math>\forall\, L \in \operatorname{List}(A) : L * [\,] = L</math>. Теперь пусть применяется конструктор: <math>a : L</math>. Необходимо доказать, что <math>(a : L) * [\,] = a : L</math>. Это делается при помощи применения второго клоза определения функции <math>\operatorname{append}</math>:
<math>(a : L) * [\,] = a : (L * [\,]) = a : (L) = a : L</math>.
'''Пример 24. Доказать [[w:Ассоциативная операция|ассоциативность]] функции <math>\operatorname{append}</math>.'''
#
<math>([\,] * L_2) * L_3 = (L_2) * L_3 = L_2 * L_3</math>.
<math>[\,] * (L_2 * L_3) = (L_2 * L_3) = L_2 * L_3</math>.
# Пусть для списков <math>L_1</math>, <math>L_2</math> и <math>L_3</math> ассоциативность функции <math>\operatorname{append}</math> доказана. Необходимо доказать для <math>(a : L_1)</math>, <math>L_2</math> и <math>L_3</math>:
<math>\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)</math>.
<math>(a : L_1) * (L_2 * L_3) = a : \Big(L_1 * (L_2 * L_3)\Big)</math>.
Как видно, последние два выведенных выражения равны, так как для списков <math>L_1</math>, <math>L_2</math> и <math>L_3</math> ассоциативность полагается доказанной.
'''Пример 25. Доказательство тождества двух определений функции <math>\operatorname{reverse}</math>.'''
Определение 1:
<math>\operatorname{reverse}\ (H : T) = (\operatorname{reverse}\ T) * [H]</math>
Определение 2:
<math>\operatorname{rev}\ (H : T)\ L = \operatorname{rev}\ T\ (H : L)</math>
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что:
<math>\forall\, L \in \operatorname{List}(A) : \operatorname{reverse}\ L = \operatorname{reverse}'\; L</math>.
<math>\operatorname{reverse}\ [\,] = [\,]</math>.
<math>\operatorname{reverse}'\; [\,] = \operatorname{rev}\ [\,]\ [\,] = [\,]</math>.
2. Шаг — пусть для списка <math>L</math> тождество функций <math>\operatorname{reverse}</math> и <math>\operatorname{reverse}'</math> доказано. Необходимо доказать его для списка <math>(H : L)</math>.
<math>\operatorname{reverse}\ (H : L) = (\operatorname{reverse}\ L) * [H] = (\operatorname{reverse}'\; L) * [H]</math>.
<math>\operatorname{reverse}'\; (H : L) = \operatorname{rev}\ (H : L)\ [\,] = \operatorname{rev}\ L\ (H : [\,]) = \operatorname{rev}\ L\ [H]</math>.
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом <math>A</math>. Это также делается по индукции:
2.1. Базис — <math>L = [\,]</math>:
<math>(\operatorname{reverse}'\; [\,]) * [H] = (\operatorname{rev}\ [\,]\; [\,]) * [H] = [\,] * [H] = [H]</math>.
<math>\operatorname{rev}\ [\,]\ [H] = [H]</math>.
2.2. Шаг — <math>L = (A : T)</math>:
<math>\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]</math>.
<math>\operatorname{rev}\ (A : T)\ [H] = \operatorname{rev}\ L\ (A : H)</math>.
Здесь произошло выпадение в [[w:Дурная бесконечность|дурную бесконечность]]. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут всё усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.
Индукционная гипотеза: <math>(\operatorname{reverse}'\; L_1) * L_2 = \operatorname{rev}\ L_1\ L_2</math>. Эта индукционная гипотеза является обобщением выражения <math>(\operatorname{reverse}'\; L) * [H] = \operatorname{rev}\ L\ [H]</math>.
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 2.2 выглядит следующим образом:
<math>= \Big((\operatorname{reverse}'\; T) * [A]\Big) * L_2 = (\operatorname{reverse}'\; T) * ([A] * L_2) = (\operatorname{reverse}'\; T) * (A : L_2)</math>.
<math>\operatorname{rev}\ (A : T)\ L_2 = \operatorname{rev}\ T\ (A : L_2) = (\operatorname{reverse}'\; T) * (A : L_2)</math>.
Что и требовалось доказать.
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых [[w:Эвристика|эвристических]] шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.
|