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

Вставлены формулы, взятые с http://roman-dushkin.narod.ru/fp_09.html
м
(Вставлены формулы, взятые с http://roman-dushkin.narod.ru/fp_09.html)
{{ОФП Содержание}}
 
Формальная задача: пусть имеется набор функций <math>f = <f1\langle f_1,\, ...\ldots,\, fnf_n \rangle</math>, определённых на областях <math>D = <D1\langle D_1,\, ...\ldots,\, DnD_n \rangle</math>. Требуется доказать, что для любого набора значений <math>d</math> имеет место некоторое свойство, т.е.то есть:
 
<math>\forall\, d \in D : P\Big(f(d)\Big)</math>,
,
 
где <math>P</math> — рассматриваемое свойство. Например:
#
#
#
 
<math>\forall\, d \in D : f(d) \geqslant 0</math>
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, т.е. справедливые для всей области D.
 
<math>\forall\, d \in D : f(d) = f\Big(f(d)\Big)</math>
Далее рассматриваются некоторые виды областей определения D...
 
<math>\forall\, d \in D : f(d) = f_1(d)</math>
'''1. D — линейно упорядоченное множество.'''
 
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, то есть справедливые для всей области <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:Отношение порядка|отношение порядка]].
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа D.
 
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести [[w:Математическая индукция|индукцию]] по данным. То есть достаточно доказать два пункта:
'''2. D — определяется как индуктивный класс'''
 
#<math>P\Big(f(\varnothing)\Big)</math> — базис индукции;
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант di = 0,n  D, либо набор первичных типов Ai = 0,n : d  Ai  d  D. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы g1, ..., gm, определённые над Ai и D, и справедливо, что:
#<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 \Big(f (d)\Big)</math> необходимо доказать для базиса класса;
# Шаг индукции: <math>P \Big(f (d)\Big) = P \bigg(f \Big(gi g_i(d)\Big)\bigg)</math>.
 
Например, для доказательства свойств функций для списков (тип <math>\operatorname{List }(A)</math>), достаточно доказать рассматриваемое свойство для двух следующих случаев:
 
# <math>P \Big(f ([\,])\Big)</math>.
# <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 }(A)</math>) можно проводить на основе следующей индукции:
 
# <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 }(A)</math> и самой функции <math>\operatorname{append}</math> (в инфиксной записи используется символ <math>*</math>).
 
# <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>.'''
 
Т.е.То есть необходимо доказать, что для любых трехтрёх списков L1<math>L_1</math>, L2<math>L_2</math> и L3<math>L_3</math> имеет место равенство <math>(L1L_1 * L2L_2) * L3L_3 = L1L_1 * (L2L_2 * L3L_3)</math>. При доказательстве индукция будет проводиться по первому операнду, т.е.то есть списку L1<math>L_1</math>:
 
#L1 <math>L_1 = [\,]</math>:
([] * L2) * L3 = (L2) * L3 = L2 * L3.
[] * (L2 * L3) = (L2 * L3) = L2 * L3.
#Пусть для списков L1, L2 и L3 ассоциативность функции append доказана. Необходимо доказать для (a : L1), L2 и L3:
((a : L1) * L2) * L3 = (a : (L1 * L2)) * L3 = a : ((L1 * L2) * L3).
(a : L1) * (L2 * L3) = a : (L1 * (L2 * L3)).
 
<math>([\,] * L_2) * L_3 = (L_2) * L_3 = L_2 * L_3</math>.
Как видно, последние два выведенных выражения равны, т.к. для списков L1, L2 и L3 ассоциативность полагается доказанной.
<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>.
'''Пример 25. Доказательство тождества двух определений функции reverse.'''
<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}\ [\,] = [\,]</math>
 
reverse (H : T) = (reverse T) * [H]
<math>\operatorname{reverse}\ (H : T) = (\operatorname{reverse}\ T) * [H]</math>
 
Определение 2:
 
<math>\operatorname{reverse}'\; L = \operatorname{rev}\ L [\,]</math>
<math>\operatorname{rev}\ [\,]\ L = L</math>
 
rev (H : T) L = rev T (H : L)
<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>.
.
 
#1.&nbsp;Базис — <math>L = [\,]</math>:
reverse [] = [].
reverse’ [] = rev [] [] = [].
#Шаг — пусть для списка L тождество функций reverse и reverse’ доказано. Необходимо доказать его для списка (H : L).
reverse (H : L) = (reverse L) * [H] = (reverse’ L) * [H].
reverse’ (H : L) = rev (H : L) [] = rev L (H : []) = rev L [H].
 
<math>\operatorname{reverse}\ [\,] = [\,]</math>.
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом A. Это также делается по индукции:
##Базис — L = []:
(reverse’ []) * [H] = (rev [] []) * [H] = [] * [H] = [H].
rev [] [H] = [H].
##Шаг — L = (A : T):
(reverse’ (A : T)) * [H] = (rev (A : T) []) * [H] = (rev T (A : [])) * [H] = (rev T [A]) * [H].
rev (A : T) [H] = rev L (A : H).
 
<math>\operatorname{reverse}'\; [\,] = \operatorname{rev}\ [\,]\ [\,] = [\,]</math>.
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут все усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.
2.&nbsp;Шаг — пусть для списка <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>.
Индукционная гипотеза: (reverse’ L1) * L2 = rev L1 L2. Эта индукционная гипотеза является обобщением выражения (reverse’ L) * [H] = rev L [H].
 
<math>\operatorname{reverse}'\; (H : L) = \operatorname{rev}\ (H : L)\ [\,] = \operatorname{rev}\ L\ (H : [\,]) = \operatorname{rev}\ L\ [H]</math>.
 
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом <math>A</math>. Это также делается по индукции:
 
2.1.&nbsp;Базис — <math>L = [\,]</math>:
 
<math>(\operatorname{reverse}'\; [\,]) * [H] = (\operatorname{rev}\ [\,]\; [\,]) * [H] = [\,] * [H] = [H]</math>.
<math>\operatorname{rev}\ [\,]\ [H] = [H]</math>.
2.2.&nbsp;Шаг — <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 выглядит следующим образом:
 
(reverse’ (A : T)) * L2 = (rev (A : T) []) * L2 = (rev T [A]) * L2 = ((reverse’ T) * [A]) * L2 = = (reverse’ T) * ([A] * L2) = (reverse’ T) * (A : L2).
rev<math>\Big(\operatorname{reverse}'\; (A : T)\Big) L2* L_2 = (\operatorname{rev T}\ (A : L2T)\ [\,]) * L_2 = (reverse’\operatorname{rev}\ T\ [A]) * (AL_2 : L2).=</math>
 
<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:Эвристика|эвристических]] шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.