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

Материал из Викиучебника — открытых книг для открытого мира
Содержимое удалено Содержимое добавлено
мНет описания правки
Вставлены формулы, взятые с http://roman-dushkin.narod.ru/fp_09.html
Строка 2: Строка 2:
{{ОФП Содержание}}
{{ОФП Содержание}}


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


<math>\forall\, d \in D : P\Big(f(d)\Big)</math>,
,


где P — рассматриваемое свойство. Например:
где <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>.


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


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


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


#P (f ([])).
# <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>.
# .


Доказательство свойств функций над S-выражениями (тип S-expr (A)) можно проводить на основе следующей индукции:
Доказательство свойств функций над <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. Доказать, что .'''
'''Пример 23. Доказать, что <math>\forall\, L \in \operatorname{List}(A) : L * [\,] = L</math>.'''


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


#L = [] : [] * [] = [] = L. Базис индукции доказан.
# <math>L = [\,] : [\,] * [\,] = [\,] = L</math>. Базис индукции доказан.
# . Теперь пусть применяется конструктор: a : L. Необходимо доказать, что (a : L) * [] = a : L. Это делается при помощи применения второго клоза определения функции append:
# <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. Доказать ассоциативность функции append.'''
'''Пример 24. Доказать [[w:Ассоциативная операция|ассоциативность]] функции <math>\operatorname{append}</math>.'''


Т.е. необходимо доказать, что для любых трех списков L1, L2 и L3 имеет место равенство (L1 * L2) * L3 = L1 * (L2 * L3). При доказательстве индукция будет проводиться по первому операнду, т.е. списку L1:
То есть необходимо доказать, что для любых трёх списков <math>L_1</math>, <math>L_2</math> и <math>L_3</math> имеет место равенство <math>(L_1 * L_2) * L_3 = L_1 * (L_2 * L_3)</math>. При доказательстве индукция будет проводиться по первому операнду, то есть списку <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:
Определение 1:


reverse [] = []
<math>\operatorname{reverse}\ [\,] = [\,]</math>

reverse (H : T) = (reverse T) * [H]
<math>\operatorname{reverse}\ (H : T) = (\operatorname{reverse}\ T) * [H]</math>


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


reverse' L = rev L []
<math>\operatorname{reverse}'\; L = \operatorname{rev}\ L [\,]</math>
rev [] L = L
<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>.
.


#Базис — L = []:
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 выглядит следующим образом:
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 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 (A : T) L2 = rev T (A : L2) = (reverse’ T) * (A : L2).
<math>\Big(\operatorname{reverse}'\; (A : T)\Big) * L_2 = (\operatorname{rev}\ (A : T)\ [\,]) * L_2 = (\operatorname{rev}\ T\ [A]) * L_2 =</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:Эвристика|эвристических]] шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.

Версия от 16:02, 26 января 2008

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

,

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

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

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

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 выглядит следующим образом:

.

.

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

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