Доказательство правильности программ (стр. 6 )

Такой способ доказательства правильности для рекурсивных функций естествен, поскольку он следует основной схеме вычислений в рекурсивных программах. Студенты уже, конечно, обратили внимание на то, что этапы 1 и 2 фактически являются этапами доказательства с помощью индукции, но индукция осуществляется «по структуре» данных, которые обрабатывает программа. В частности, если можно сопоставить интуитивное понятие более простых данных (допустимых аргументов функции) и более сложных с отношением во вполне упорядоченном множестве значений данных (допустимых аргументов функции), то этапы 1 и 2 будут аналогичны этапам доказательства правильности работы программы для всех допустимых аргументов с помощью метода обобщенной индукции. Предложенный выше способ доказательства правильности назовем доказательством с помощью структурной индукции. Проиллюстрируем этот метод на нескольких очень простых рекурсивных программах.

Пример 4.6. Докажем правильность следующей программы (разд. 4.1, пример 4.1):

F(Х) º IF X = 1 ТНЕN 1

ЕLSЕ ОТНЕRWISЕ X•F(Х – 1)

Предполагается, что эта функция вычисляет факториал от аргумента. Нужно доказать, что F(М) = 1 • 2 • 3 • ... • N = N! для любого положительного числа N. При доказательстве с помощью структурной индукции используем простую индукцию по положительным целым числам:

1) докажем, что F(1)= 1!. Действительно, F(1)= 1=1!;

2) докажем (для любого положительного числа N), что если
F(М) = 1 • 2 • ... • N = N!, то F(N + 1) = 1 • 2 • ... • N • (N + 1) = (N + 1)!. Следовательно, мы предполагаем, что N – положительное число, а F(N) = N! – гипотеза индукции. Так как N положительное число, то проверка N + 1 = 1 дает отрицательный ответ, и, прослеживая далее последовательность вычислений, получаем

F(N + 1) = (N + 1) • F((N + 1) – 1) = (N + 1) • F(N) =
= (N +1) • (N!) = (N +1) • (1 • 2 • ... • N) = 1 • 2 • ... • N • (N +1) = (N +1)!

(По гипотезе
индукции)

что и требовалось доказать, т. е. F(N) = N! для любого положительного числа N.

Пример 4.7. Докажем правильность следующей программы (разд. 4.1, примера 4.4):

МЕМВЕR (Х, L) º IF L = NIL THEN FALSЕ

ЕLSЕ IF Х = CAR(L) ТНЕN TRUE

ЕLSЕ ОТНЕRWISЕ МЕМВЕR (X, CDR(L))

Эта программа применима для любого элемента X и любого списка L. Предполагается, что она дает значение ТRUЕ, если X входит в качестве элемента верхнего уровня в список L; в противном же случае она дает значение FALSЕ:

МЕМВЕR (Х, L¢) = TRUE, если X элемент списка L¢
= FALSЕ в других случаях.

Для доказательства правильности работы этой программы используем структурную индукцию. Анализ программы показывает, что при рекурсивном обращении к МЕМВЕR из третьей строки программы только второй аргумент обращения выглядит проще, чем ранее. Таким образом, естественно вести индукцию только по второму аргументу функции. При рекурсивном обращении к МЕМВЕR ее второй аргумент CDR (L) представляет собой список, который содержит на один элемент (на верхнем уровне) меньше, чем список L. Следовательно, в структурной индукции можно использовать простую индукцию по числу элементов в списке L. Так как это число всегда неотрицательно, то доказательство основывается на простой индукции по неотрицательным целым числам. Итак, нужно:

1) доказать, что для любого списка, содержащего нуль элементов, МЕМВЕR работает правильно. Поскольку список, имеющий нуль элементов, это просто пустой список NIL, то очевидно, что МЕМВЕR (Х, NIL) = FALSЕ, так как X не есть элемент списка NIL;

2) доказать (для любого целого числа N), что если программа МЕМВЕR правильно работает для всех списков L¢, содержащих N элементов (на верхнем уровне), то она будет правильно работать и для всех списков L, содержащих на верхнем уровне (N + 1) элементов. Поэтому предположим, что МЕМВЕR правильно работает для списков L¢ длиной N, т. е.

МЕМВЕR (Х, L¢) = TRUE если X есть элемент из L¢,

= FALSЕ в других случаях.

Это гипотеза индукции. Предположим, что L есть список, содержащий (N + 1) элементов. Поскольку (N + 1) ³ 1, то L ¹ NIL. Прослеживая выполнение функции, видим, что

МЕМВЕR (Х, L) = TRUE если X = CAR (L),

= МЕМВЕR (Х, CDR (L)) в других случаях.

Если X = CAR(L) (а мы знаем, что CAR(L) определено, так как L¹NIL), то X – элемент списка L, и, следовательно, значение TRUЕ есть именно то значение, которое требуется. Если Х ¹ CAR (L), то X будет элементом списка L, если и только если X будет элементом CDR (L). (Функция CDR (L) определена, так как L ¹ NIL.) Однако CDR (L) представляет собой список из N элементов, и по гипотезе индукции следует, что МЕМВЕR (Х, СDR (L)) будет правильно вычислять значение TRUE или FALSЕ в зависимости от того, является ли X элементом CDR (L) или нет. Таким образом, если Х ¹ CDR (L), то МЕМВЕR (Х, L) = МЕМВЕR (Х, CDR (L)), а последняя функция вычисляет значение либо TRUЕ, либо FALSЕ в зависимости от того, будет ли X элементом CDR (L), а следовательно, элементом списка L или нет, что и требовалось доказать.

Пример 4.8. Докажем правильность следующей рекурсивной программы (разд. 4.1, пример 4.5):

АРРЕND (L1, L2) º IF L1 = NIL ТНЕN L2
ЕLSЕ ОТНЕRWISE СONS (CAR (L1),
АРРЕND (CDR (L1, L2))

Предполагается, что программа применима к любым двум спискам L1 и L2 и в качестве результата дает список, состоящий из элементов списка L1, за которым следуют элементы списка L2. Анализ программы показывает, что при рекурсивном обращении к АРРЕND только первый из ее двух аргументов выглядит проще, чем ранее. Таким образом, при доказательстве методом структурной индукции используем простую индукцию по длине (числу элементов) списка L1. Для этого необходимо:

1. Доказать правильность работы АРРЕND для любого списка L1 длиной 0. Список длиной нуль – пустой список NIL. Утверждение АРРЕND (NIL, L2) = L2 правильно, так как это список, составленный из элементов списка L1 (а он пустой), за которыми следуют элементы списка L2.

2. Доказать для любых неотрицательных целых чисел N, что если АРРЕND правильно работает для любых списков L1¢ длиной N, то АРРЕND будет правильно работать и для всех списков L1 длиной (N + 1). Предположим, что АРРЕND для всех списков L1¢ длиной N работает правильно, т. е. АРРЕND (L1¢, L2) есть список, составленный из элементов L1¢, за которыми следуют элементы списка L2. (Это гипотеза индукции.) Предположим, что длина списка L1 равна (N + 1). Так как (N +1) ³ 1, то L1 ¹ NIL. Прослеживая вычисление функции, мы видим, что

АРРЕND(L1, L2) = CONS (CAR (L1), АРРЕND (CDR (L1), L2))

(Известно, что CAR (L1 и CDR (L1) определены, ибо L1 ¹ NIL.) Однако CDR (L1) – список длиной N, и из гипотезы индукции следует, что АРРЕND (CDR (L1), L2) есть список, состоящий из элементов CDR (L1) и элементов списка L2. Таким образом, список АРРЕND (CDR (L1), L2) содержит все элементы списка L1, кроме первого, за которыми идут все элементы списка L2. Кроме того, так как СОNS (CAR (L1), АРРЕND (CDR (L1), L2)) образует список, у которого первый элемент CAR (L1), а затем следуют элементы списка АРРЕND (CDR (L1), L2), то очевидно, что этот список состоит из всех элементов списка L1 (включая и первый элемент CAR (L1)) и всех элементов списка L2. Следовательно, в этом случае функция АРРЕND работает правильно, что и требовалось доказать.

Замечание

В начале раздела мы уже говорили о том, что если можно было бы сопоставить наше интуитивное представление о простоте данных (допустимых аргументов функции) с некоторым вполне упорядочивающим отношением < на множестве значений данных, то доказательство правильности для рекурсивных программ можно было бы проверить методом обобщенной индукции по этим данным. Отметим, что в примере 4.6 мы проводили доказательство именно этим методом, поскольку данными этой функции были целые числа, а обычное отношение < вполне упорядочивает соответствующие значения. В примерах же 4.7 и 4.8 такого отношения <, определенного на множестве значений данных для наших программ (это были списки), уже не было. Вместо него мы использовали тот факт, что вполне упорядоченным было множество некоторых свойств значений данных, а именно длины. Длина любого списка – неотрицательное целое число, а обычное отношение < вполне упорядочивает множество неотрицательных целых чисел. Если мы хотим определить отношение < не на множестве некоторого из свойств данных, а на самих данных (в нашем случае списках), то это можно сделать следующим образом: будем говорить, что L1 < L2, если и только если длина L1< длины L2. К несчастью, для вполне упорядочивающего порядка этого недостаточно, так как отношение < определяет лишь частичный, а не общий порядок. Например, при L1 = [А В С] и L2 = [D Е F] мы не можем сказать, что L1 < L2, или L2 < L1, или L1 = L2. Другими словами, существуют данные (списки одинакового размера), не сравнимые между собой, и, следовательно, порядок, заданный отношением <, не является общим. Таким образом, наше множество не будет вполне упорядоченным; иногда такие множества называют обоснованно упорядоченными (well-founded). Оказывается, что существования обоснованного порядка (который более общий, чем вполне упорядочивающий) достаточно для проведения доказательства по индукции. Таким образом, в примерах 4.7 и 4.8 доказательство можно было бы проводить с помощью обобщенной индукции по данным, упорядоченным на основе обоснованного порядка. Обоснованный порядок < можно было бы и превратить во вполне упорядочивающий, если списки равной длины считать не несравнимыми, а равными; но это уже несколько неуклюжий прием. Далее мы будем продолжать проводить индукцию на множестве некоторых свойств данных (таких, как длина) и не беспокоиться по поводу формального определения типа существующего порядка.

В качестве упражнений решите следующие задачи:

а) рассмотрите следующую рекурсивную программу, применимую для любого положительного целого числа N:

F(N) º IF N = 1 ТНЕN 1
ЕLSЕ ОТНЕRWISЕ F(N – 1) + N,

и докажите, что F(N) = (N • (N + 1) )/2 при любом положительном целом N;

б) рассмотрите рекурсивную программу, применимую для любых неотрицательных целых чисел N: