John Harrison - Введение в функциональное программирование (1108517), страница 22
Текст из файла (страница 22)
Нам потребуется определить подходящее для этого вида индукцииотношение, причём такое, что результаты последующих рекурсивных вызововпредшествуют предыдущим; это гарантирует завершимость алгоритма. В общемслучае, для этого могут понадобиться сложные отношения, заданные на аргументах,но часто бывает достаточно придумать меру, которая отображает аргументы нанатуральные числа и убывает в ходе рекурсии. В данном случае такой мерой можетслужить |y|.Теорема 7.2 Для произвольных целых x и y, вычисление gcd x y завершается срезультатом, равным НОД x и y.Доказательство: Предположим для некоторого n, что для произвольногозначения x и y такого, что |y| < n теорема справедлива. Основываясь наэтом предположении, попробуем доказать, что она справедлива также дляпроизвольного x при |y| = n.
Этого будет достаточно, чтобы считать теоремудоказанной, поскольку для любого y найдётся некоторое n такое, что |y| =n. Согласно определению функции, доказательство разбивается на два частныхслучая.• Предположим, что y = 0. В этом случае по определению функции gcd x y = x.Очевидно, x|x и x|0, т. е. является общим делителем. Предположим, чтонайдётся ещё один общий делитель d, для которого справедливо d|x и d|0.Отсюда немедленно следует d|x, из чего, в свою очередь, вытекает то, что xявляется НОД.• Рассмотрим случай y6=0. Мы хотим применить индуктивноепредположение к gcd y (x mod y). Введём сокращённое обозначение r = x mod y.Основным свойством функции mod является то, что при y 6= 0 найдётсятакое целое q, что x = qy + r и |r| < |y|.
Поскольку |r| < |y|, из индуктивногопредположения следует, что d = gcd y (x mod y) является НОД y и r.Остаётся показать, что он является НОД также и для x и y. Очевидно,это также справедливо, поскольку при d|y и d|r мы имеем d|x, таккак x = qy + r. Предположим, что d0 |x и d0 |y.
Аналогично сказанному выше,обнаруживаем, что d0 |r. Таким образом, d0 является общим делителем y и r,а по индуктивному предположению d0 |d, что и требовалось.86Глава 7. Доказательство корректности программ7.4. Конкатенация списковОтметим, что в доказательстве было использовано основное свойство операциивычисления остатка. Её реализация (функция mod) в конкретных CAML-системахтребует тщательной проверки соответствия теоретическому определению. Хорошоизвестно, что различные языки программирования (и даже реализации одного итого же языка) зачастую различаются в трактовке операции вычисления остаткав случае отрицательных аргументов. Если отсутствует уверенность в надёжностинеявных предположений, их можно добавить в теорему в явной форме.7.4Конкатенация списковРассмотрим пример верификации функции, оперирующей списками.Функция append предназначена, как это следует из её названия, для конкатенации(сцепления) двух списков.
Например, результатом применения этой операции кспискам [3; 2; 5] и [6; 3; 1] будет [3; 2; 5; 6; 3; 1].#let rec append l1 l2 =match l1 with[] -> l2| (h::t) -> h::(append t l2);;Данная функция вводится при помощи примитивной рекурсии в соответствиис определением списочного типа. Она определяется для случая пустого списка и,затем, для списка вида h :: t, причём в последнем случае используется значениеэтой же функции для аргумента t. Следовательно, доказательства теорем о еёсвойствах удобно строить на соответствующем принципе структурной индукциидля списков: если некоторое утверждение справедливо для пустого списка и, еслииз предположения, что оно выполняется для t следует, что данное утверждениесправедливо и для h :: t, то мы можем заключить, что оно справедливо для любогосписка.
Однако, такой подход не обязателен — при желании можно воспользоватьсяматематической индукцией по длине списка. Докажем с учётом сказанного выше,что операция конкатенации ассоциативна.Теорема 7.3 Для трёх произвольных списков l1 , l2 и l3 справедливо:append l1 (append l2 l3 ) = append (append l1 l2 ) l3Доказательство: Применяя структурную индукцию к l1 , докажем, что требуемоесвойство выполняется для произвольных l2 и l3 .• Если l1 = [], то:append l1 (append l2 l3 ) ====87append [] (append l2 l3 )append l2 l3append (append [] l2 ) l3append (append l1 l2 ) l37.5.
Обращение списковГлава 7. Доказательство корректности программ• Рассмотрим случай l1 = h :: t. Предположим, что для l2 и l3 мы имеемappend t (append l2 l3 ) = append (append t l2 ) l3Отсюда следуетappend l1 (append l2 l3 ) ======append (h :: t) (append l2 l3 )h :: (append t (append l2 l3 ))h :: (append (append t l2 ) l3 )append (h :: (append t l2 )) l3 )append (append (h :: t) l2 ) l3 )append (append l1 l2 ) l3 )7.5Обращение списковОпределить функцию обращения списков несложно:#let rec rev =fun [] -> []| (h::t) -> append (rev t) [h];;rev : ’a list -> ’a list = <fun>#rev [1;2;3];;- : int list = [3; 2; 1]Докажем, что функция rev является инволюцией, т.
е. чтоrev(rev l) = lОднако, если мы попытаемся напрямую применить структурную индукцию,оказывается, что нам понадобится сперва доказать пару дополнительных лемм.Лемма 7.4 Для произвольного списка l справедливо append l [] = l.Доказательство: Воспользуемся структурной индукцией по l.• Для l = [] имеем:append l [] = append [] []= []= l• Пусть l = h :: t. Предполагая, что append t [] = t, получимappend l [] ====88append (h :: t) []h :: (append t [])h :: tlГлава 7.
Доказательство корректности программ7.5. Обращение списковЛемма 7.5 Для произвольных списков l1 и l2 справедливоrev(append l1 l2 ) = append (rev l2 ) (rev l1 )Доказательство: Для доказательства этой леммы также воспользуемсяструктурной индукцией по l1 .• При l1 = [] получаемrev(append l1 l2 ) ====rev(append [] l2 )rev l2append (rev l2 )[]append (rev l2 ) (rev [])• Если l1 = h :: t и мы знаем, чтоrev(append t l2 ) = append (rev l2 ) (rev t)то из этого следуетrev(append l1 l2 ) =======rev(append (h :: t) l2 )rev(h :: (append t l2 ))append (rev(append t l2 )) [h]append (append (rev l2 ) (rev t)) [h]append (rev l2 ) (append (rev t) [h])append (rev l2 ) (rev (h :: t))append (rev l2 ) (rev l1 )Теорема 7.6 Для произвольного списка l справедливо rev(rev l) = l.Доказательство: Применим структурную индукцию по l.• При l = [] имеем:rev(rev l) ====rev(rev [])rev [][]l• Пусть l = h :: t и справедливо, чтоrev(rev t) = t897.5.
Обращение списковГлава 7. Доказательство корректности программв этом случае мы получим:rev(rev l) ============rev(rev (h :: t))rev(append (rev t) [h])append (rev [h]) (rev(rev t))append (rev [h]) tappend (rev (h :: [])) tappend (append (rev []) [h]) tappend (append [] [h]) tappend [h] tappend (h :: []) th :: (append [] t)h :: tlБольшое количество теорем о свойствах операций над списками может бытьдоказано в аналогичном стиле. Доказательство в целом базируется на структурнойиндукции, применяемой к списку. В некоторых случаях может оказаться удобнымвыделить части рассуждений в отдельные леммы, которые также доказываютсяиндуктивно, кроме того, задача может потребовать обобщения, прежде чем индукцияокажется применимой.
Некоторые примеры таких задач приведены в упражнениях.Дополнительная литератураВ работе Neumann (1995) приведён обзор рисков, связанных как сраспространением компьютеров в обществе в целом, так и с последствиямипрограммных ошибок в частности. Очень интересная дискуссия с примерамина эту же тему даётся в Peterson (1996). Применимость верификации являласьв своё время предметом споров; некоторые аргументы против этого подходаизложены в DeMillo, Lipton, and Perlis (1979). Также заслуживает вниманияобоснованное обсуждение Barwise (1989).
На данный момент количество публикацийпо верификации велико, но в большинстве своём они рассматривают императивныепрограммы. Некоторые учебники функционального программирования дляначинающих, такие как Paulson (1991) и Reade (1989), включают базовые примерынаподобие рассмотренных в данной книге. Представляет интерес работа Boyerand Moore (1979), авторы которой провели верификацию свойств определенийчистых функций на языке LISP при помощи своей системы автоматизированногодоказательства теорем. Одним из самых масштабных опытов по верификации,наподобие рассмотренных здесь, служит применение данной методики к программеупрощения логических выражений, которая используется в синтезе СБИС Aagaardand Leeser (1994).90Глава 7.
Доказательство корректности программ7.5. Обращение списковУпражнения1. Докажите корректность более эффективного алгоритма возведения в степень:#let square x = x * x;;#let rec exp x n =if n = 0 then 1else if n mod 2 = 0 then square(exp x (n / 2))else x * square(exp x (n / 2));;2. Пусть функция length определена как#let rec length =fun [] -> 0| (h::t) -> 1 + length t;;Докажите, что length(rev l) = length l и что length(append l1 l2 ) = length l1 +length l2 .3. Определим функцию map, которая применяет заданную функцию к каждомуэлементу списка, следующим образом:#let rec map f =fun [] -> []| (h::t) -> (f h)::(map f t);;Докажите, что если l 6= [] то hd(map f l) = f (hd l) и map f (rev l) =rev (map f l). Далее, используя следующее определение композиции функций,#let o f g = fun x -> f(g x);;#infix "o";;докажите, что map f (map g l) = map (f ◦ g) l.4.
Функция «91» Мак-Карти может быть определена так:#let rec f x = if x > 100 then x - 10else f(f(x + 11));;Докажите, что для n ≤ 101 справедливо f (n) = 91. Особое внимание следуетуделить доказательству завершимости. (Указание: возможно использоватьмеру 101 − x.)917.5. Обращение списковГлава 7.
Доказательство корректности программ5. Задача о голландском флаге состоит в сортировке списка «цветов» (красный,белый, синий) так, чтобы цвета расположились в данном порядке. Требуетсярешить задачу, используя исключительно перестановку соседних элементов.Пример решения на языке ML приводится ниже. Функция dnf возвращаетзначение true тогда и только тогда, когда порядок следования элементовизменился; её вычисление повторяется, пока на некотором этапе не окажется,что изменений не обнаружено.type c o l o u r = Red | White | Blue ; ;l e t rec dnf =fun [ ] −> [ ] , f a l s e| ( White : : Red : : r e s t ) −> Red : : White : : r e s t , t r u e| ( Blue : : Red : : r e s t ) −> Red : : Blue : : r e s t , t r u e| ( Blue : : White : : r e s t ) −> White : : Blue : : r e s t , t r u e| ( x : : r e s t ) −> l e t f l , ch = dnf r e s t in x : : f l , ch ; ;l e t rec f l a g l =l e t l ’ , changed = dnf l ini f changed then f l a g l ’ e l s e l ’ ; ;Например,#flag [White; Red; Blue; Blue; Red; White; White; Blue; Red];;- : colour list =[Red; Red; Red; White; White; White; Blue; Blue; Blue]Докажите, что функция flag всегда завершается, и её результатом будеткорректно упорядоченный список.6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
