Основы функционального программирования/Доказательство свойств функций: различия между версиями
мНет описания правки |
Вставлены формулы, взятые с http://roman-dushkin.narod.ru/fp_09.html |
||
Строка 2: | Строка 2: | ||
{{ОФП Содержание}} |
{{ОФП Содержание}} |
||
Формальная задача: пусть имеется набор функций f = |
Формальная задача: пусть имеется набор функций <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 |
#<math>P\Big(f(d)\Big)</math> необходимо доказать для базиса класса; |
||
#Шаг индукции: P |
# Шаг индукции: <math>P\Big(f(d)\Big) = P\bigg(f\Big(g_i(d)\Big)\bigg)</math>. |
||
Например, для доказательства свойств функций для списков (тип List |
Например, для доказательства свойств функций для списков (тип <math>\operatorname{List}(A)</math>), достаточно доказать рассматриваемое свойство для двух следующих случаев: |
||
#P |
# <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 |
Доказательство свойств функций над <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 |
Для доказательства этого свойства можно использовать только определение типа <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>.''' |
||
То есть необходимо доказать, что для любых трёх списков <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>: |
|||
# |
# <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: |
||
<math>\operatorname{reverse}\ [\,] = [\,]</math> |
|||
reverse (H : T) = (reverse T) * [H] |
|||
<math>\operatorname{reverse}\ (H : T) = (\operatorname{reverse}\ T) * [H]</math> |
|||
Определение 2: |
Определение 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. Базис — <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. Шаг — пусть для списка <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. Базис — <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 выглядит следующим образом: |
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 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). |
|||
<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. — линейно упорядоченное множество.
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, то есть:
.
В качестве примера можно привести множество целых чисел. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить отношение порядка.
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. То есть достаточно доказать два пункта:
- — базис индукции;
- — шаг индукции.
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа .
2. — определяется как индуктивный класс
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант , либо набор первичных типов . Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы , определённые над и , и справедливо, что:
.
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:
- необходимо доказать для базиса класса;
- Шаг индукции: .
Например, для доказательства свойств функций для списков (тип ), достаточно доказать рассматриваемое свойство для двух следующих случаев:
- .
- .
Доказательство свойств функций над -выражениями (тип ) можно проводить на основе следующей индукции:
- .
- .
Пример 23. Доказать, что .
Для доказательства этого свойства можно использовать только определение типа и самой функции (в инфиксной записи используется символ ).
- . Базис индукции доказан.
- . Теперь пусть применяется конструктор: . Необходимо доказать, что . Это делается при помощи применения второго клоза определения функции :
.
Пример 24. Доказать ассоциативность функции .
То есть необходимо доказать, что для любых трёх списков , и имеет место равенство . При доказательстве индукция будет проводиться по первому операнду, то есть списку :
- :
.
.
- Пусть для списков , и ассоциативность функции доказана. Необходимо доказать для , и :
.
.
Как видно, последние два выведенных выражения равны, так как для списков , и ассоциативность полагается доказанной.
Пример 25. Доказательство тождества двух определений функции .
Определение 1:
Определение 2:
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что:
.
1. Базис — :
.
.
2. Шаг — пусть для списка тождество функций и доказано. Необходимо доказать его для списка .
.
.
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом . Это также делается по индукции:
2.1. Базис — :
.
.
2.2. Шаг — :
.
.
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут всё усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.
Индукционная гипотеза: . Эта индукционная гипотеза является обобщением выражения .
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 2.2 выглядит следующим образом:
.
.
Что и требовалось доказать.
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.