Основы функционального программирования/Доказательство свойств функций: различия между версиями
Пока лишь копия текста из MS Word - необходима стилизация |
Первоначальная викификация |
||
Строка 1: | Строка 1: | ||
Лекция 9. «Доказательство свойств функций» |
= Лекция 9. «Доказательство свойств функций» = |
||
Формальная задача: пусть имеется набор функций f = <f1, ..., fn>, определённых на областях D = <D1, ..., Dn>. Требуется доказать, что для любого набора значений d имеет место некоторое свойство, т.е.: |
Формальная задача: пусть имеется набор функций f = <f1, ..., fn>, определённых на областях D = <D1, ..., Dn>. Требуется доказать, что для любого набора значений d имеет место некоторое свойство, т.е.: |
||
, |
|||
где P — рассматриваемое свойство. Например: |
где P — рассматриваемое свойство. Например: |
||
# |
|||
# |
|||
# |
|||
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, т.е. справедливые для всей области D. |
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, т.е. справедливые для всей области D. |
||
Далее рассматриваются некоторые виды областей определения D... |
Далее рассматриваются некоторые виды областей определения D... |
||
1. D — линейно упорядоченное множество. |
'''1. D — линейно упорядоченное множество.''' |
||
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, т.е.: |
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, т.е.: |
||
. |
|||
В качестве примера можно привести множество целых чисел. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить отношение порядка. |
В качестве примера можно привести множество целых чисел. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить отношение порядка. |
||
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. Т.е. достаточно доказать два пункта: |
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. Т.е. достаточно доказать два пункта: |
||
⚫ | |||
# — базис индукции; |
|||
⚫ | |||
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа D. |
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа D. |
||
2. D — определяется как индуктивный класс |
'''2. D — определяется как индуктивный класс''' |
||
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант di = 0,n D, либо набор первичных типов Ai = 0,n : d Ai d D. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы g1, ..., gm, определённые над Ai и D, и справедливо, что: |
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант di = 0,n D, либо набор первичных типов Ai = 0,n : d Ai d D. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы g1, ..., gm, определённые над Ai и D, и справедливо, что: |
||
. |
|||
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост: |
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост: |
||
#P (f (d)) необходимо доказать для базиса класса; |
|||
#Шаг индукции: P (f (d)) = P (f (gi (d))). |
|||
Например, для доказательства свойств функций для списков (тип List (A)), достаточно доказать рассматриваемое свойство для двух следующих случаев: |
Например, для доказательства свойств функций для списков (тип List (A)), достаточно доказать рассматриваемое свойство для двух следующих случаев: |
||
#P (f ([])). |
|||
2. . |
|||
# . |
|||
Доказательство свойств функций над S-выражениями (тип S-expr (A)) можно проводить на основе следующей индукции: |
Доказательство свойств функций над S-выражениями (тип S-expr (A)) можно проводить на основе следующей индукции: |
||
1. . |
|||
# . |
|||
# . |
|||
⚫ | |||
⚫ | |||
Для доказательства этого свойства можно использовать только определение типа List (A) и самой функции append (в инфиксной записи используется символ *). |
Для доказательства этого свойства можно использовать только определение типа List (A) и самой функции append (в инфиксной записи используется символ *). |
||
#L = [] : [] * [] = [] = L. Базис индукции доказан. |
|||
# . Теперь пусть применяется конструктор: a : L. Необходимо доказать, что (a : L) * [] = a : L. Это делается при помощи применения второго клоза определения функции append: |
|||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
Т.е. необходимо доказать, что для любых трех списков L1, L2 и L3 имеет место равенство (L1 * L2) * L3 = L1 * (L2 * L3). При доказательстве индукция будет проводиться по первому операнду, т.е. списку L1: |
Т.е. необходимо доказать, что для любых трех списков L1, L2 и L3 имеет место равенство (L1 * L2) * L3 = L1 * (L2 * L3). При доказательстве индукция будет проводиться по первому операнду, т.е. списку L1: |
||
#L1 = []: |
|||
([] * L2) * L3 = (L2) * L3 = L2 * L3. |
|||
[] * |
([] * 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 = a : ((L1 * L2) * L3). |
||
(a : L1) * (L2 * L3) = a : (L1 * (L2 * L3)). |
(a : L1) * (L2 * L3) = a : (L1 * (L2 * L3)). |
||
Как видно, последние два выведенных выражения равны, т.к. для списков L1, L2 и L3 ассоциативность полагается доказанной. |
Как видно, последние два выведенных выражения равны, т.к. для списков L1, L2 и L3 ассоциативность полагается доказанной. |
||
Пример 25. Доказательство тождества двух определений функции reverse. |
'''Пример 25. Доказательство тождества двух определений функции reverse.''' |
||
Определение 1: |
Определение 1: |
||
⚫ | |||
reverse (H : T) = (reverse T) * [H] |
reverse [] = [] |
||
reverse (H : T) = (reverse T) * [H] |
|||
Определение 2: |
Определение 2: |
||
reverse' L = rev L [] |
|||
reverse' L = rev L [] |
|||
⚫ | |||
⚫ | |||
rev [] L = L |
|||
⚫ | |||
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что: |
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что: |
||
⚫ | |||
. |
|||
1. Базис — L = []: |
|||
reverse [] = []. |
|||
#Базис — L = []: |
|||
⚫ | |||
⚫ | |||
reverse’ [] = rev [] [] = []. |
|||
⚫ | |||
⚫ | |||
reverse (H : L) = (reverse L) * [H] = (reverse’ L) * [H]. |
|||
⚫ | |||
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом A. Это также делается по индукции: |
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом A. Это также делается по индукции: |
||
##Базис — L = []: |
|||
(reverse’ []) * [H] = (rev [] []) * [H] = [] * [H] = [H]. |
(reverse’ []) * [H] = (rev [] []) * [H] = [] * [H] = [H]. |
||
rev [] [H] = [H]. |
rev [] [H] = [H]. |
||
##Шаг — L = (A : T): |
|||
(reverse’ (A : T)) * [H] = (rev (A : T) []) * [H] = (rev T (A : [])) * [H] = (rev T [A]) * [H]. |
(reverse’ (A : T)) * [H] = (rev (A : T) []) * [H] = (rev T (A : [])) * [H] = (rev T [A]) * [H]. |
||
rev (A : T) [H] = rev L (A : H). |
rev (A : T) [H] = rev L (A : H). |
||
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут все усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере. |
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут все усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере. |
||
Индукционная гипотеза: (reverse’ L1) * L2 = rev L1 L2. Эта индукционная гипотеза является обобщением выражения (reverse’ L) * [H] = rev L [H]. |
Индукционная гипотеза: (reverse’ L1) * L2 = rev L1 L2. Эта индукционная гипотеза является обобщением выражения (reverse’ L) * [H] = rev L [H]. |
||
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 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). |
(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). |
rev (A : T) L2 = rev T (A : L2) = (reverse’ T) * (A : L2). |
||
Что и требовалось доказать. |
Что и требовалось доказать. |
||
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество. |
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество. |
Версия от 09:28, 7 февраля 2006
Лекция 9. «Доказательство свойств функций»
Формальная задача: пусть имеется набор функций f = <f1, ..., fn>, определённых на областях D = <D1, ..., Dn>. Требуется доказать, что для любого набора значений d имеет место некоторое свойство, т.е.:
,
где P — рассматриваемое свойство. Например:
Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, т.е. справедливые для всей области D.
Далее рассматриваются некоторые виды областей определения D...
1. D — линейно упорядоченное множество.
Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, т.е.:
.
В качестве примера можно привести множество целых чисел. Однако линейно упорядоченные множества встречаются в мире функционального программирования очень редко. Взять хотя бы простейшую структуру, которую очень любят обрабатывать в функциональном программировании — список. Для списков уже довольно сложно определить отношение порядка.
Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. Т.е. достаточно доказать два пункта:
- — базис индукции;
- — шаг индукции.
В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа D.
2. D — определяется как индуктивный класс
Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант di = 0,n D, либо набор первичных типов Ai = 0,n : d Ai d D. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы g1, ..., gm, определённые над Ai и D, и справедливо, что:
.
В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:
- P (f (d)) необходимо доказать для базиса класса;
- Шаг индукции: P (f (d)) = P (f (gi (d))).
Например, для доказательства свойств функций для списков (тип List (A)), достаточно доказать рассматриваемое свойство для двух следующих случаев:
- P (f ([])).
- .
Доказательство свойств функций над S-выражениями (тип S-expr (A)) можно проводить на основе следующей индукции:
- .
- .
Пример 23. Доказать, что .
Для доказательства этого свойства можно использовать только определение типа List (A) и самой функции append (в инфиксной записи используется символ *).
- L = [] : [] * [] = [] = L. Базис индукции доказан.
- . Теперь пусть применяется конструктор: a : L. Необходимо доказать, что (a : L) * [] = a : L. Это делается при помощи применения второго клоза определения функции append:
.
Пример 24. Доказать ассоциативность функции append.
Т.е. необходимо доказать, что для любых трех списков L1, L2 и L3 имеет место равенство (L1 * L2) * L3 = L1 * (L2 * L3). При доказательстве индукция будет проводиться по первому операнду, т.е. списку L1:
- L1 = []:
([] * 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)).
Как видно, последние два выведенных выражения равны, т.к. для списков L1, L2 и L3 ассоциативность полагается доказанной.
Пример 25. Доказательство тождества двух определений функции reverse.
Определение 1:
reverse [] = [] reverse (H : T) = (reverse T) * [H]
Определение 2:
reverse' L = rev L [] rev [] L = L rev (H : T) L = rev T (H : L)
Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что:
.
- Базис — L = []:
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].
Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом 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).
Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут все усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.
Индукционная гипотеза: (reverse’ L1) * L2 = rev L1 L2. Эта индукционная гипотеза является обобщением выражения (reverse’ L) * [H] = rev L [H].
Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 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).
Что и требовалось доказать.
Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.