1. Нашёл ошибку?
2. Выдели её мышью.
3. Нажми Ctrl-Enter.

[ закрыть ]

Лекция 9. "Доказательство свойств функций"

Понравились лекции? Используете их для обучения? Можете отблагодарить автора:

рублей Яндекс.Деньгами
на счет 4100137733052 (Лекции по Функциональному программированию)

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

,

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




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

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

1. D — линейно упорядоченное множество.

Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, т.е.:

.

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

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

  1. — базис индукции;
  2. — шаг индукции.

В силу того, что структуры данных редко образуют линейно упорядоченные множества, более эффективным способом оказывается применение метода индукции по построению типа D.

2. D — определяется как индуктивный класс

Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант di = 0,n in D, либо набор первичных типов Ai = 0,n : d in Ai => d in D. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы g1, ..., gm, определённые над Ai и D, и справедливо, что:

.

  1. P (f (d)) необходимо доказать для базиса класса;
  2. Шаг индукции: P (f (d)) = P (f (gi (d))).

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

  1. P (f ([])).
  2. .

Доказательство свойств функций над S-выражениями (тип S-expr (A)) можно проводить на основе следующей индукции:

  1. .
  2. .

Пример 23. Доказать, что .

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

  1. L = [] : [] * [] = [] = L. Базис индукции доказан.
  2. . Теперь пусть применяется конструктор: a : L. Необходимо доказать, что (a : L) * [] = a : L. Это делается при помощи применения второго клоза определения функции append:

.

Пример 24. Доказать ассоциативность функции append.

Т.е. необходимо доказать, что для любых трех списков L1, L2 и L3 имеет место равенство (L1 * L2) * L3 = L1 * (L2 * L3). При доказательстве индукция будет проводиться по первому операнду, т.е. списку L1:

1°. L1 = []:

([] * L2) * L3 = (L2) * L3 = L2 * L3.
[] * (L2 * L3) = (L2 * L3) = L2 * L3.

2°. Пусть для списков 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)

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

.

1. Базис — L = []:

reverse [] = [].
reverse' [] = rev [] [] = [].

2. Шаг — пусть для списка 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. Это также делается по индукции:

2.1. Базис — L = []:

(reverse' []) * [H] = (rev [] []) * [H] = [] * [H] = [H].
rev [] [H] = [H].

2.2. Шаг — 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).

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

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

Наверх | Содержание | Лекции | НАУКА ·]

Сайт управляется системой uCoz