Сборник задач по курсу «Теория вычислительных процессов» (стр. 10 )

Пример 8.1. Докажем правильность рекурсивной программы, рассмотренной в примере 7.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(N) = 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.

Аналогично используется структурная индукция для доказательства правильности рекурсивных программ, работающих со списками. Однако доказательство в этом случае оказывается несколько более сложным.

Пример 8.2. Докажем правильность рекурсивной программы, работающий со списками, рассмотренной в  примере 7.2:

МЕМВЕ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 или нет, что и требовалось доказать.

Упражнения

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

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

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

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

F(N)  ≡  IF  N = 0  ТНЕN  1
ЕLSЕ  ОТНЕRWISЕ  2 • F(N – 1),

выведите формулу для вычисляемой функции F(N) и докажите ее правильность.

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

F(N)  ≡  IF  N = 0  ТНЕN  0
ЕLSЕ  ОТНЕRWISЕ  F (F(N – 1)).

Докажите, что F(N) = 0 для любого неотрицательного целого числа N.

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

F(N)  ≡  IF  N ≤ 1  ТНЕN N
ЕLSЕ  ОТНЕRWISЕ  F (N – 2).

Докажите, что для всякого четного неотрицательного целого числа функция F равна 0, т. е. F(2 • N) = 0 для всех неотрицательных целых N. Кроме того, докажите, что для каждого нечетного неотрицательного целого числа значение F равно 1.

5. Докажем правильность следующей рекурсивной программы

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

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

6. Рекурсивная программа применима для любых списков L:

REVERS (L)  ≡  IF  L = NIL  ТНЕN  NIL
ЕLSЕ ОТНЕRWISE  АРРЕND (REVERS
(CDR (L), СONS (CAR (L), NIL))

Докажите, что для любого списка L результат работы REVERS (L) представляет собой список, содержащий те же элементы, что и список L, но размещенные в обратном порядке. Замечание: при доказательстве можно исходить из того, что АРРЕND работает правильно (это доказано в упражнении 5).

7. Рекурсивная программа применима к любому объекту X и любому списку L:

DELETE1 (X, L)  ≡  IF  L = NIL  ТНЕN  NIL
ЕLSЕ  IF  X = CAR (L)  ТНЕN CDR (L)
ЕLSЕ ОТНЕRWISE  СONS (CAR (L),
DELETE1 (X, CDR (L)))

Докажите, что DELETE1 (X, L) для любого списка L представляет собой список, полученный вычеркиванием из L первого вхождения элемента X на верхнем уровне (если он там есть). Например,

DELETE1 (B, [A [B] B C B]) = [A [B] C B].

8. Опишите рекурсивную программу DELETE (X, L), которая вычеркивает  из L все вхождения на верхнем уровне объекта X. Докажите, что ваша программа работает правильно.

9. Две приведенные ниже функции применимы к любым двум множествам, представляемым списками. Множество есть список без повторяющихся элементов, т. е. ни один из любых двух элементов не равен другому:

INT (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  NIL
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
СONS (CAR (L1), INT (CDR (L1), L2))
ЕLSЕ ОТНЕRWISE  INT (CDR (L1), L2)

UNION (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  L2
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
       UNION (CDR (L1), L2))
ЕLSЕ ОТНЕRWISE  СONS (CAR (L1),
       UNION (CDR (L1), L2))

Докажите, что для любых двух множеств L1 и L2 результат работы INT (L1, L2) представляет пересечение (множество) L1 и L2, а UNION (L1, L2) – объединение множеств L1 и L2:

INT (L1, L2) = множество (список без повторяющихся элементов), которое содержит элементы, имеющиеся в списках L1 и L2.

UNION (L1, L2) = множество (список без повторяющихся элементов), которое содержит элементы, имеющиеся либо в L1, либо в L2, либо в L1 и в L2.

При проведении доказательства можно предположить, что функция
MEMBER, рассмотренная в примере 8.2, работает правильно.

10. Рассмотрите следующую рекурсивную программу, аргументами которой могут быть два любые множества L1 и L2:

F1 (L1, L2)  ≡  IF  L1 = NIL  ТНЕN  TRUE
ЕLSЕ  IF  MEMBER (CAR (L1), L2)  ТНЕN
       F (CDR (L1), L2)
ЕLSЕ ОТНЕRWISE  FALSE

Выясните, что делает эта программа, и докажите ваше утверждение.

11. Рассмотрите две рекурсивные программы (LEAST применима к любому непустому списку L1, состоящему из чисел, а SORT применима к любому списку L2, состоящему из чисел):

LEAST (L1)  ≡  IF CDR (L1) = NIL  ТНЕN  CAR (L1)
ЕLSЕ  IF  CAR (L1)  ≤ LEAST (CDR (L1))  ТНЕN  CAR (L1)
ЕLSЕ  ОТНЕRWISE  LEAST (CDR (L1))

SORT (L2)  ≡  IF  L2 = NIL  ТНЕN  L2
ЕLSЕ  ОТНЕRWISE  CONS (LEAST (L2), SORT
(DELETE1 (LEAST (L2), L2)))

Докажите, что для любого непустого числового списка L2 программа SORT (L2) дает список L2, упорядоченный в неубывающем порядке. Для этого вначале докажите, что при любом непустом числовом списке L1 программа LEAST (L1) дает наименьшее число из списка L1. Указание: при проведении доказательства можно предположить, что функция DELETE1 работает так, как описано в упражнении 7.