Сдам Сам

ПОЛЕЗНОЕ


КАТЕГОРИИ







Рекурсивные функции работы со списками





Рекурсивные программы особенно удобны в тех случаях, когда речь идет о данных, структура которых определяется рекурсивно, каковыми являются, например, списки. Рассмотрим примеры работы со списками, считая, что список – набор объектов, отделенных друг от друга пробелами и заключенных в квадратные скобки [ ]. Объектами, входящими в такие списки, являются атомы или другие списки. Атом – строка буквенно-цифровых символов, не содержащая пробелов. Мы будем считать, что атомы должны начинаться с одной из букв А, В, С, D или F. Например, [А В С] – список из трех элементов, каждый из которых есть атом; [А [В А [С]] В С] – список, в котором (на верхнем уровне) четыре элемента. Второй элемент – сам список [В А [С]]. Для пустого списка, т.е. списка, не содержащего ни одного элемента, мы выделяем специальное имя NIL. Кроме того, мы будем использовать следующие проверки и функции:

1. Проверка = может применяться как к спискам, так и к числам. Например, проверка [А В] = [А В] истинна, а проверки [А В] = [В А] ложна.

2. Проверка АТОМ (X) применима к любым объектам, будь то атомы или списки и дает значение TRUE, если X – атом или пустой список, иначе – FALSE.

3. Функция CAR (L) применима к любому непустому списку. В качестве результата выступает первый элемент этого списка: CAR ( [А В С] ) дает А.

4. Функция CDR(L) применима к любому непустому списку. Результатом является список, полученный из L путем отбрасывания первого его элемента. Примеры: CDR ( [А В С] ) дает [В С], CDR ( [В] )дает NIL (или [ ] ).

5. Функцию CONS(Х, L) можно применять к любому списку L и любому X, будь то атом или список. В результате получается новый список: первый его элемент есть X, а потом идут элементе списка L. Так CONS ( А, [В С] ) дает [А В С].

Пример 7.2. Рекурсивная программа МЕМВЕR (Х, L) определяет, является ли X элементом списка L (на верхнем уровне):

МЕМВЕR (Х, L) º IF L = NIL ТНЕN FALSE

ЕLSЕ IF Х = САR (L) ТНЕN TRUE

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

Проследим, как идет процесс вычислений по такой программе для фактических аргументов С и [А В С D]:

МЕМВЕR (С, [А В С D]) = МЕМВЕR (С, [В С D]) = МЕМВЕR (С, [С В]) = TRUЕ

Вычисление значения функции при фактических аргументах С и [А В [С D]]:

МЕМВЕR (С, [А В [С D]]) = МЕМВЕR (С, [В [С D]] ) = МЕМВЕR (С, [[С В]] ) =
= МЕМВЕR (С, NIL) = FALSE

Упражнения

6. Рекурсивная программа APPEND (L1, L2), добавляет список L1 к списку L2, другими словами, в этом списке, состоящем из двух, элементы первого стоят перед элементами второго:

APPEND (L1, L2) º IF L1 = NIL ТНЕN L2
ЕLSЕ OTHERWISE CONS (CAR (L1),
АРРЕND (CDR(L1), L2))

Проследите, как идет процесс вычислений при различных парах аргументов:

а) АРРЕND ([А В], [С D]); б) АРРЕND ([[А]], [В С]);

с) АРРЕND ([А В], NIL); г) АРРЕND (NIL, [А В С]);

д) АРРЕND ([А В [С]], [D]); е) АРРЕND ([А В], [[С] D]).

7. Для рекурсивной программы, применимой к любым двум спискам L1, L2:

INT (L1, L2) º IF L1 = NIL ТНЕN NIL

ЕLSЕ IF МЕМВЕR (САR (L1), L2) ТНЕN

CONS (САR (L1), INT (CDR (L1), L2))

ЕLSЕ ОТНЕRWISЕ INT (CDR (L1), L2)



Выпишите последовательность вычислений для случаев

а) INT (NIL, [А В С]); б) INT ([B D C], [А В С]);

в) INT ([[B D] C], [А В D]). г) INT ([С В А], [А В С]);

Тема 8. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ
РЕКУРСИВНЫХ ПРОГРАММ

Структурная индукция

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

1) доказать, что программа работает правильно для простейших данных (аргументов функции);

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

Такой способ доказательства правильности для рекурсивных функций естествен, поскольку он следует основной схеме вычислений в рекурсивных программах. Назовем его доказательством с помощью структурной индукции.

Пример 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 работает правильно.

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

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

Приложение

Задание на итоговую самостоятельную работу
по теме «Доказательство правильности программ»

Вариант № 1

  1. Доказать с помощью простой индукции, что для любого положительного n

2 + 4 + 6 + … + (2n – 2) + 2n = n(n + 1).

  1. Доказать правильность блок-схемы программы, вычисляющей 2n

Указание: приписать индуктивные утверждения (о входных данных, о правильности, о конечности и инвариант цикла) точкам 1, 2 и 3. Доказать, что утверждение-инвариант действительно является инвариантом (для доказательства использовать простую индукцию). Из инварианта цикла и утверждения о конечности получить утверждение о правильности блок-схемы.

3. Доказать правильность программы, написанной на VBA.

SUB ПРИМЕР( )

M = CELLS (1, 1) Указание: приписать индуктивные утверждения

N = CELLS (1, 2) (о входных данных, о правильности, о конечности

I = 1: J = M и инвариант цикла) нужным точкам программы,

DO WHILE (I < N) оформив в виде комментариев и доказать правиль-

J = J×M ность программы аналогично предыдущему случаю

I = I + 1

LOOP

CELLS (1, 3) = J

END SUB

4. Написать аксиомы верификации для оператора языка VBA

{A1} Указание:для облегчения работы необходимо

DO UNTIL C изобразить соответствующий фрагмент блок-схемы

S

LOOP

{A2}

5. Доказать правильность рекурсивной программы методом структурной индукции (для положительных значений аргумента N). Гипотеза: F(2N) = N(N+1)

F(2N) º IF N = 1 THEN 2

ELSE OTHERWISE 2N + F(2N –2)

6. Сформулируйте и запишите формализованное условие верификации на пути из точки 2 в точку 2 блок-схемы из задания 2.

Литература

1. Веретельникова Е.Л. Доказательство правильности программ: Метод индуктивных утверждений. Конспект лекций. – Новосибирск, Изд-во НГТУ, 2004. – 59 с.

2. Веретельникова Е.Л. Доказательство правильности программ: Дополнительные приемы. Конспект лекций. – Новосибирск, Изд-во НГТУ, 2005. – 36 с.

3. Андерсен Р. Доказательство правильности программ. – М.: Мир, 1982. – 163 с.

4. Информатика. Теория и практика структурного программирования: Методическая разработка. – Новосибирск, изд-во НГТУ, 1999.

5. Лингер Р., Миллс Х., Уитт Б. Теория и практика структурного программирования. / Пер. с англ., М.: Мир, 1982.

6. Хопкрофт Дж., Мотвани Р., Нильман Дж. Введение в теорию автоматов, языков и вычислений, 2-е изд. – М.: Изд. дом «Вильямс», 2002.

7. Метод индуктивных утверждений для доказательства правильности программ: Учебное пособие. – Новосибирск, 2002. – В электронном виде.

8. Кнут Д. Искусство программирования для ЭВМ. – М.: «Мир», Т. 1, 1976.

9. Романов Е.Л. Практикум по программированию на С++: Уч. пособие. СПб: БХВ-Петербург; Новосибирск: Изд-во НГТУ, 2004. – 432 с.

СОДЕРЖАНИЕ

Тема 1. МАТЕМАТИЧЕСКАЯ ИНДУКЦИЯ.............................................................................. 3

Принцип простой индукции.......................................................................................... 3

Принцип модифицированной простой индукции.................................................... 3

Принцип строгой индукции.......................................................................................... 7

Тема 2. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ БЛОК-СХЕМ ПРОГРАММ................ 10

Основные принципы доказательства правильности для блок-схем................. 10

Тема 3. МЕТОД ИНДУКТИВНЫХ УТВЕРЖДЕНИЙ............................................................ 15

Описание метода индуктивных утверждений........................................................ 16

Тема 4. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ,
НАПИСАННЫХ НА ОБЫЧНЫХ ЯЗЫКАХ ПРОГРАММИРОВАНИЯ............. 23

Тема 5. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности
С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ................................................ 27

Тема 6. АКСИОМАТИЧЕСКИЙ ПОДХОД К ДОКАЗАТЕЛЬСТВУ ЧАСТИЧНОЙ ПРАВИЛЬНОСТИ........................................................................................................................................... 32

Тема 7. РЕКУРСИВНЫЕ ПРОГРАММЫ.................................................................................. 35

Введение понятие рекурсии....................................................................................... 36

Рекурсивные функции работы со списками............................................................ 39

Тема 8. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ РЕКУРСИВНЫХ ПРОГРАММ........... 41

Структурная индукция................................................................................................. 41

Задание на итоговую самостоятельную работу по теме «Доказательство правильности программ».............................................................................. 46

Литература................................................................................................................................ 47

 









Не нашли то, что искали? Воспользуйтесь поиском гугл на сайте:


©2015- 2018 zdamsam.ru Размещенные материалы защищены законодательством РФ.