Теория вычислительных процессов Лекция ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ РЕКУРСИВНЫХ ПРОГРАММ Преподаватель: Веретельникова Евгения Леонидовна 1
ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ РЕКУРСИВНЫХ ПРОГРАММ ВВЕДЕНИЕ Во многих языках программирования разрешается писать рекур- сивные программы, т.е. программы, в которых при вычислениях допускается обращение (рекурсивное) к самой себе аналогично тому, как обычная, нерекурсивная программа обращается к некото- рой подпрограмме. Рекурсивные программы особенно удобны в тех случаях, когда речь идет о данных, структура которых определя- ется рекурсивно (например, списки или деревья). В языке Лисп, созданном специально для «нечисленных» вычислений на основе списков, понятие рекурсии является фундаментальным. В этой главе описаны методы, которые полезны при доказательстве правиль- ности рекурсивных программ. Основной метод в таких доказатель- ствах называется методом структурной индукции. Доказательство методом структурной индукции представляет собой доказательство с помощью математической индукции, но индукция осуществляется по структуре данных, с которыми работает программа. Если студент незнаком с понятием рекурсии, он все равно сможет понимать излагаемый здесь материал. Мы не будем пользоваться каким-нибудь стандартным рекурсивным языком программирования, например Алголом или Лиспом, а «изобретем» упрощенный язык, которого нам будет достаточно, чтобы проиллюстрировать понятие рекурсии. В разд. 4.1 введен такой язык, в разд. 4.2 описан метод структурной индукции, а примеры рассмотрены в разд В разд. 4.4 показано, что метод структурной индукции может оказаться полезным и в тех случаях, когда речь идет о нерекурсивных программах. В частности, показано, что метод структурной индукции иногда легче использовать для доказательства правильности, чем метод индуктивных утверждении, если, например, речь идет о нерекурсивных программах, выполняющих рекурсивные по существу процессы, такие, как просмотр деревьев. 2
ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ РЕКУРСИВНЫХ ПРОГРАММ Если вы незнакомы с понятием рекурсии, то все равно сможете понимать излагаемый здесь материал. Мы не будем пользоваться каким-нибудь стандартным рекурсивным языком программирова- ния, например Алголом или Лиспом, а «изобретем» упрощенный язык, которого нам будет достаточно, чтобы проиллюстрировать понятие рекурсии. Далее введен такой язык, а после описан метод структурной индукции и рассмотрены примеры. Можно показать, что метод структурной индукции может оказаться полезным и в тех случаях, когда речь идет о нерекурсивных программах. В частности, показано, что метод структурной индукции иногда легче использовать для доказательства правильности, чем метод индуктивных утверждении, если, например, речь идет о нерекурсивных программах, выполняющих рекурсивные по существу процессы, такие, как просмотр деревьев. 3
Упрощенный язык программирования для иллюстрации понятия рекурсии Упрощенный язык программирования нужен нам, чтобы ознакомиться с понятием рекурсии. Если вы знакомы с рекурсией в каком-либо из существующих языков программирования, вам будет очень просто сопоставить наш упрощенный язык с соответ- ствующими возможностями в этих реальных языках. Однако, если вы даже и незнакомы с понятием рекурсии из существующих язы- ков, это не помешает вам понять содержание данного раздела. Программа в нашем упрощенном языке программирования состоит из определения функции, заданного в виде F(Х1,..., ХN) IF проверка 1 THEN выражение 1 ELSE IF проверка 2 THEN выражение 2. : ELSE IF проверка m THEN выражение m ELSE OTHERWISE выражение m + 1 4
Упрощенный язык программирования для иллюстрации понятия рекурсии Такая программа вычисляет значение F(Х1,..., ХN). Сначала выполняется проверка 1. Если проверка 1 дает ответ «истина», то значение функции есть значение выражения 1. Если проверка 1 дает ответ «ложь», то выполняется проверка 2. Если эта проверка дает ответ «истина», то значение функции есть значение выражения 2. Процесс идет таким образом до тех пор, пока не будет обнаружена первая из проверок (i-я), дающая значение «истина». Значение функции в этом случае есть значение выражения i. Если ни одна из проверок не окажется положи- тельной, то значение функции есть значение выражения m
Упрощенный язык программирования для иллюстрации понятия рекурсии Рекурсия вводится в этот язык программирования следующим образом: функция F, определяемая в нашей программе, может входить как часть в любое из выражений или проверок в программе. Такое появление F называется рекурсивным обращением к этой функции. Для каждой такой рекурсивной программы нужно еще указать, для каких значений аргументов X1,..., ХN применима программа, т.е. нужно задать область определения функции. Выполнение программы заключается в применении ее к некоторым конкретным данным из ее области определения. 6
ПРИМЕР 1 Рассмотрим рекурсивную программу, определенную для любого положительного целого числа X: F(Х) IF Х = 1 THEN 1 ELSE OTHERWISE XF(Х–1) Чтобы понять, как работает такая программа, выполним ее для некоторого конкретного значения аргумента X. Например, F(4) = 4F(3)[Так как условие 4 = 1 ложно, то F(4)=4F(3). Теперь нужно вычислить F(3), т.е. рекурсивно обратиться к F.] = 43F(2)[Т. к. при вычислении F(3) условие 3=1 ложно, то F(3) = 3F(2).] = 432F(1) [Так как условие 2 = 1 ложно, то F(2) = 2F(1).] = 4321[Так как условие 1 = 1 истинно, то F(1) = 1.] = 24 = 4 ! Ниже мы докажем, что F(Х) = Х ! для любого положительного целого числа X. Пример 4.2. Рассмотрим следующую рекурсивную функцию (функцию Аккермана), применимую для любой пары неотрицательных целых чисел X1, Х2: А(Х1, Х2) IF X1 = 0 THEN Х2 + 1 ELSE IF Х2=0 THEN А(Х1–1, 1) ELSE OTHERWISE А(Х1–1, А(Х1, Х2–1)) Проследим, как выполняется такая программа для некоторой пары X1 и Х2. Например, А(1, 2) = А(0, А(1, 1))[Так как условия X1 = 0 и Х2 = 0 ложны, необходимо вычислять А(1, 1) – рекурсивное обращение.] = А(0, А(0, А(1, 0))) [Так как условия X1 = 0 и Х2 = 0 ложны, нужно вычислять А(1, 0).] = А(0, А(0, А(0, 1))) [Так как условие X1 = 0 ложно, а Х2 = 0 истинно.] = А(0, А(0, 2))[Так как X1 = 0 истинно, следовательно, А(0, 1) = = 2.] = А(0, 3)[Так как X1 =0 истинно, следовательно, А(0, 2) = = 3.] = 4[Так как X1 = 0 истинно, следовательно, А(0, 3) = 3 + 1=4.] 7
ПРИМЕР 2 Рассмотрим следующую рекурсивную функцию (функцию Аккермана), применимую для любой пары неотрицательных целых чисел X1, Х2 : А(Х1, Х2) IF X1 = 0 THEN Х2 + 1 ELSE IF Х2=0 THEN А(Х1–1, 1) ELSE OTHERWISE А(Х1–1, А(Х1, Х2–1)) Проследим выполнение программы для некоторой пары X1 и Х2: А(1, 2) = А(0, А(1, 1))[Так как условия X1 = 0 и Х2 = 0 ложны, необходимо вычислять А(1, 1) – рекурсивное обращение.] = А(0, А(0, А(1, 0))) [Так как условия X1 = 0 и Х2 = 0 ложны, нужно вычислять А(1, 0).] = А(0, А(0, А(0, 1))) [Так как условие X1 = 0 ложно, а Х2 = 0 истинно.] = А(0, А(0, 2)) [Так как X1 = 0 истинно, следовательно, А(0, 1) = = 2.] = А(0, 3) [Так как X1 =0 истинно, следовательно, А(0, 2) = = 3.] = 4 [Т. к. X1 = 0 истинно, то А(0, 3) = 3 + 1=4.] 8
ПРИМЕР 2 Из этого примера следует, что при выполнении вычислений для рекурсивной программы мы можем сталкиваться с неоднозначнос- тями, которые требуют уточнений. Например, в приведенных вычи- слениях при обращении А(0, А(1, 1)) мы предполагаем, что А(1, 1) должно быть вычислено прежде, чем мы продолжим вычисления, относящиеся к внешнему обращению к А. Если отдать предпочтение вычислениям, связанным с внешним обращением, то вычисления должны были бы идти в следующем порядке: А(1, 2) = А(0, А(1, 1)) = А(1, 1) + 1 = А(0, А(1, 0)) + 1 = = (А(1, 0) + 1) + 1 = (А(0, 1) + 1) + 1 = (2 + 1) + 1=4. Значение А(1, 2) остается тем же, хотя последовательность вычислений отлична от предыдущей. Можно доказать, что если к одним и тем же аргументам некоторой рекурсивной функции применять две различные последовательности ее вычисления, то результат будет одним и тем же при условии конечности этих последовательностей. Однако вполне возможно, что одна последовательность не будет заканчиваться, хотя другая последовательность закончится. Рассмотрим следующий пример. 9
ПРИМЕР 3 Возьмем рекурсивную программу, применимую к любой паре неотрицательных целых X1, Х2: F(Х1, Х2) IF X1 =0 ТНЕN 0 ELSE OTHERWISE F(0, F(Х1, Х2)) Проследим за вычислением F(1, 1), используя два различных правила вычислений. По первому правилу мы будем стараться сначала заканчивать вычисления, относящиеся к внешнему обращению. По второму правилу мы будем отдавать предпочтение самому внутреннему обращению: 1) F(1, 1) = F(0, F(1, 1))[Так как условие X1 = 0 ложно.] = 0[Так как условие X1 = 0 истинно для внешнего обращения к F.] 2) F(1, 1) = F(0, F(1, 1))[Так как условие X1 = 0 ложно.] = F(0, F(0, F(1, 1))) [Так как условие X1 = 0 для внутреннего обращения ложно.] = F(0, F(0, F(0, F(1, 1)))) = = F(0, F(0, F(0, F(0, F(1,1))))) и т. д. 10
ПРИМЕР 3. ВЫВОДЫ Таким образом, в первом случае последовательность вычис- лений F(1, 1) конечна и F(1, 1) = 0. Во втором случае вычисления не заканчиваются и, следовательно, значение F(1, 1) не определено. Однако отметим, что если для каких-либо аргументов в обоих случаях вычисления заканчиваются, то результат будет одним и тем же. Например, F(0, М) = 0 независимо от применяемых правил вычислений. Итак, чтобы сделать наш язык программирования точным, нам нужно задать правила вычислений для программ, определяющие последовательность вычислений. Здесь мы будем считать, что правило вычислений отдает предпочтение самому левому и самому внутреннему обращению. Другими словами, в любой из моментов вычислений первым начинает вычисляться левое и внутреннее обращение (для простоты далее везде будем опускать слово «самое») к функции F, все аргументы которой уже не содержат F. 11
ВЫВОДЫ Это правило – не обязательно наилучшее, иногда оно может приводить к неоканчивающейся последовательности вычислений, хотя другое правило дало бы конечную последовательность (пример 3). Однако во многих существующих языках программирования используется правило вычислений, подобное описанному выше. Кроме того, как мы уже отмечали, если, следуя этому правилу, вычисления заканчиваются, то результат будет тем же, что и при других правилах, приводящих к окончанию. Большинство рассматриваемых нами программ заканчивается при любых значениях аргументов независимо от того, какие правила вычислений мы используем, а следовательно, и результат в любых случаях будет одинаковым. Однако для определенности все же будем считать, что предпочтение отдается левому внутреннему обращению. 12
Работа со списками Многие из приводимых здесь примеров относятся к работе со списками. В таких программах мы используем некоторое подобие «лисповской» нотации. По этой нотации список – набор объектов, отделенных друг от друга пробелами и заключенных в квадратные скобки [ ]. Объектами, входящими в такие списки, являются атомы или другие списки. Атом – строка буквенно- цифровых символов, не содержащая пробелов. Мы будем считать, что атомы должны начинаться с одной из букв А, В, С, D или F, а переменные – с букв, отличных от этих букв. Такой прием позволяет нам при написании программ различать переменные и атомы и обходиться без более общей функции QUOTE, используемой в Лиспе. 13
Работа со списками Например, [А В С] – список из трех элементов, каждый из которых есть атом; [А [В А [С]] В С] – список, в котором (на верхнем уровне) четыре элемента. Второй элемент – сам список [В А [С]]. Третий элемент этого списка – опять список [С]. Для пустого списка, т.е. списка, не содержащего ни одного элемента, мы выделяем специальное имя NIL. Кроме того, мы будем использовать следующие проверки и функции: 1. Проверка = может применяться как к спискам, так и к числам. Например, проверка [А В] = [А В] истинна, а проверки [А В] = [В А], [А В] = [А [В]], В = А, А = NIL ложны. 2. Проверка АТОМ (X) применима к любым объектам, будь то атомы или списки. АТОМ (X) дает значение TRUE (истина), если X – атом или пустой список. Если X – непустой список, то АТОМ (X) дает значение FALSE (ложь). 14
Работа со списками 3. Функция CAR (L) применима к любому непустому списку. В качестве результата выступает первый (на верхнем уровне) элемент этого списка. Примеры: CAR ( [А В С] ) дает А. CAR ( [[А В] С] ) дает [А В]. CAR (NIL)не определено. CAR (А)не определено. 4. Функцию CDR(L) можно применять к любому непустому списку. Результатом является список, полученный из L путем отбрасывания первого его элемента (на верхнем уровне). Примеры: CDR ( [А В С] ) дает [В С]. CDR ( [[А В] С] ) дает [С]. CDR ( [В] )дает NIL (или [ ] ). CDR (NIL)не определено. CDR (А)не определено. 15
Работа со списками 5. Функцию CONS(Х, L) можно применять к любому списку L и любому X, будь то атом или список. В результате получается новый список: первый его элемент есть X, а потом идут элеме- нте списка L. Примеры: CONS ( А, [В С] )дает [А В С]. CONS ( [А В], [В [С]] ) дает [[А В] В [С]]. CONS (А, NIL)дает [А]. CONS (А, В)не определено. В некоторых из наших примеров мы будем использовать и специальные атомы ТRUЕ и FALSE. 16
Пример 4 Как пример использования новой нотации приведем рекурсивную программу, определяющую, является ли 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 17
Пример 5 Напишем рекурсивную программу, добавляющую список L1 к списку L2, другими словами, в этом списке, состоящем из двух, элементы первого стоят перед элементами второго: APPEND (L1, L2) IF L1 = NIL ТНЕN L2 ЕLSЕ OTHERWISE CONS (CAR (L1), АРРЕND (CDR(L1), L2)) Проследим, как идет процесс вычислений при нескольких различных парах аргументов: АРРЕND ([А В], [С D]) = = CONS (САR ([А В]), АРРЕND (CDR ([А В]), [С D]))) = СОNS (А, АРРЕND ([В], [С D] )) = СОNS (А, СОNS (CAR ([В]), АРРЕND (CDR([В]), [С D]))) = CONS (А, СОNS (В, АРРЕND (NIL, [С D] ))) = СОNS (А, СОNS (В, [С, D])) = СОNS (А, [В С D]) = [А В С D] 18
Пример 5 АРРЕND ([[А]], [В С] ) = СОNS ([А], АРРЕND (NIL, [В С]) = СОNS ([А], [В С]) = [[А] В С] АРРЕND([А В], NIL) = СОNS (А, АРРЕND ([В], NIL)) = СОNS (А, СОNS (В, АРРЕND (NIL, NIL))) = СОNS (А, СОNS ( [В] ) = СОNS (А, [В] ) = [А В] В качестве упражнения проследите, как проходит процесс вычисления функции Аккермана (программа приведена в примере 4.2) при следующих аргументах а) А(1,1); б) А(2,1). 19
Структурная индукция Рекурсивные программы обычно строятся по следующей схеме: сначала в них явно определяется способ вычисления результата для наипростейших значений аргументов рекурсивной функции, затем способ вычисления результата для аргументов более сложного вида, причем используется сведение к вычислениям с данными более простого вида (с аргументами рекурсивного обращения к той же функции). Таким образом, вполне естественно попытаться доказать правильность таких программ следующим образом: 1) доказать, что программа работает правильно для простейших данных (аргументов функции); 2) доказать, что программа работает правильно для более сложных данных (аргументов функции) в предположении, что она работает правильно для более простых данных (аргументов функции). 20
Структурная индукция Такой способ доказательства правильности для рекурсивных функций естествен, поскольку он следует основной схеме вычислений в рекурсивных программах. Вы уже, конечно, обратили внимание на то, что этапы 1 и 2 фактически являются этапами доказательства с помощью индукции, но индукция осуществляется «по структуре» данных, которые обрабатывает программа. В частности, если можно сопоставить интуитивное понятие более простых данных (допустимых аргументов функ- ции) и более сложных с отношением во вполне упорядоченном множестве значений данных (допустимых аргументов функции), то этапы 1 и 2 будут аналогичны этапам доказательства правиль- ности работы программы для всех допустимых аргументов с помощью метода обобщенной индукции. Предложенный выше способ доказательства правильности назовем доказательством с помощью структурной индукции. Проиллюстрируем этот метод на нескольких очень простых рекурсивных программах. 21
ПРИМЕР 6 Докажем правильность следующей программы (слайд 7): F(Х) IF X = 1 ТНЕN 1 ЕLSЕ ОТНЕRWISЕ XF(Х – 1) Предполагается, что эта функция вычисляет факториал от аргумента. Нужно доказать, что F(М) = N = N! для любого положительного числа N. При доказательстве с помощью структурной индукции используем простую индукцию по положительным целым числам: 1) докажем, что F(1)= 1!. Действительно, F(1)= 1=1!; 2) докажем (для любого положительного числа N), что если F(М) = 1 2…N = N!, то F(N + 1) = 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) ( N) = N (N +1) = (N +1)! – ЧТД, т.е. F(N) = N! для любого положительного числа N. 22
ПРИМЕР 7 Докажем правильность следующей программы ( слайд 17): МЕМВЕ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Е в других случаях. 23
ПРИМЕР 7 Для доказательства правильности работы этой программы используем структурную индукцию. Анализ программы показывает, что при рекурсивном обращении к МЕМВЕR из третьей строки программы только второй аргумент обращения выглядит проще, чем ранее. Таким образом, естественно вести индукцию только по второму аргументу функции. При рекурсивном обращении к МЕМВЕR ее второй аргумент CDR (L) представляет собой список, который содержит на один элемент (на верхнем уровне) меньше, чем список L. Следовательно, в структурной индукции можно использовать простую индукцию по числу элементов в списке L. Так как это число всегда неотрицательно, то доказательство основывается на простой индукции по неотрицательным целым числам. Итак, нужно: 24
ПРИМЕР 7 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)) в других случаях. 25
ПРИМЕР 7 Если 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 или нет, что и требовалось доказать. 26
ПРИМЕР 8 Докажем правильность следующей рекурсивной программы (слайд 18): АРРЕ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. 27
ПРИМЕР 8 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)) 28
ПРИМЕР 8 (Известно, что 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 работает правильно, что и требовалось доказать. 29
УПРАЖНЕНИЯ В качестве упражнений решите следующие задачи: а) рассмотрите следующую рекурсивную программу, применимую для любого положительного целого числа N: F(N) IF N = 1 ТНЕN 1 ЕLSЕ ОТНЕRWISЕ F(N – 1) + N, и докажите, что F(N) = (N (N + 1) )/2 при любом положительном целом N; б) рассмотрите рекурсивную программу, применимую для любых неотрицательных целых чисел N: F(N) = IF N = 0 ТНЕN 1 ЕLSЕ ОТНЕRWISЕ 2 F(N – 1), выведите формулу для вычисляемой функции F(N) и докажите ее правильность. 30
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ До сих пор для доказательства правильности нерекурсивных (итеративных) программ нами использовался введен метод индуктивных утверждений. Однако если нерекурсивная программа фактически выполняет рекурсивный процесс, то при доказательстве ее правильности иногда легче использовать метод структурной индукции, а не метод индуктивных утверждений. Сейчас мы рассмотрим пример, иллюстрирующий подобный случай. Пример 9. Мы хотим доказать, что если выполнять программу, блок-схема которой приведена на рис. 4.1, с TREE, представля- ющим собой указатель на корневую вершину некоторого двоичного дерева (TREE =, если дерево пустое), то в конце концов выполнение ее закончится, причем будут просмотрены в некотором порядке все вершины этого дерева. 31
32 Рис. 4.1
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ ( Для ознакомления с используемой в блок-схеме нотацией и алгоритмами просмотра двоичных деревьев см. стр в книге Д Кнута «Искусство программирования для ЭВМ», том 1, изд-во «Мир», ) Просмотр идет следующим образом: для каждой вершины дерева просматри- ваются одним и тем же способом все вершины левого поддерева, выходящего из данного, затем сама исходная вершина, а затем в том же порядке все вершины правого поддерева. Наша програм- ма фактически реализует некоторый рекурсивный процесс, и ее можно было бы легко написать в «рекурсивной форме». В нашей же нерекурсивной версии алгоритм основан на использовании явного стека. Мы могли бы доказать, что программа правильна, и методом индуктивных утверждений (попробуйте проделать это самостоятельно в качестве упражнения), однако рекурсивность самого процесса приводит к предположению, что это доказате- льство удобнее провести с помощью структурной индукции. 33
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ Сначала докажем, что справедливо утверждение, связанное в блок-схеме с точкой 2. При доказательстве используется структурна, индукция по размеру (числу вершин) дерева, на которое указывает Р. Для этого необходимо: 1. Доказать, что если размер дерева, на которое указывает Р, равен нулю, то утверждение справедливо. Но если размер дерева, задаваемого Р, равен нулю, то наше утверждение тривиально, ибо мы попадаем в точку 2 с пустым деревом, которое можно считать уже просмотренным в соответствующем порядке (ведь просматри- вать нечего), причем Р =, а SТАСK остался без изменений. 2. Доказать (для всех n > 0), что если наше утверждение верно для всех деревьев размером меньше n (гипотеза индукции), то оно также справедливо и для дерева размером n. Предположим, что мы находимся в точке 2 и Р = Р 0 =, затем переходим из точки 2 через точки 3, 4 вновь в точку 2. 34
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ При возвращении в точку 2 Р указывает на левое поддерево первоначального дерева, на которое указывало Р (т.е. Р = LLINK(Р 0 )), а SТАСК в состоянии SТАСК 0,Р 0 (т.е. значение Р 0 уже помещено в вершину стека). Так как размер дерева, на которое теперь указывает Р, меньше n, то мы знаем (по гипотезе индукции), что если мы когда-нибудь вернемся в точку 2, то это левое поддерево уже будет просмотрено в соответствующем порядке и, кроме того, Р =, а SТАСК опять будет в состоянии SТАСК 0,Р 0. Так как Р =, пройдем по пути из точки 2 через точки 6, 7, 8 вновь в точку 2. Вернувшись в точку 2, будем иметь Р = PLINK(Р 0 ), а SТАСК – в состоянии SТАСК 0. Исходная вершина будет уже просмотрена. Таким образом, уже будут просмотрены в соответствующем порядке вершины левого поддерева и корень (исходная вершина) дерева. Указатель Р теперь будет «смотреть» на правое поддерево; оно меньше дерева, на которое указывал Р 0. 35
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ Опять можно использовать гипотезу индукции и сделать заключение, что, если в конце концов мы вернемся в эту точку, дерево, на которое указывает Р, будет просмотрено (это правое поддерево исходного дерева), Р = и SТАСК будет в состоянии SТАСК 0. В этот момент оказывается, что мы просмотрели левое поддерево, корневую вершину и правое поддерево. Но из этого следует, что мы в соответствующем порядке просмотрели все исходное дерево. Причем Р =, а SТАСК – в состоянии SТАСК 0, что и требовалось доказать. 36
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ Изложенное доказательство легко приводит нас и к доказательству правильности, так как при первом попадании в точку 2 (из точки 1) Р = ТRЕЕ, а SТАСК пуст. Только что доказанное утверждение, связанное с точкой 2, гласит, что при попадании в точку 2 поддерево, на которое указывал Р, будет уже надлежащим образом просмотрено и SТАСК будет в исходном состоянии (пуст), а Р =. В этот момент, так как Р =, мы попадем в точку 5, так как SТАСК пуст, далее – в точку 10; это и показывает справедливость утверждения о правильности, связанного с точкой
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ В общем случае, интересно сравнить для нерекурсивных (итеративных) программ доказательство методом индуктивных утверждений с доказательством методом структурной индукции. Доказательства методом индуктивных утверждений фактически являются доказательством с помощью индукции по числу попаданий (в цикле) в некоторую точку программы. Доказательства с помощью структурной индукции также являются доказательствами по индукции, но индукция проводится по структуре данных, с которыми работает программа. Безусловно, именно структура данных определяет, сколько раз мы попадем в различные точки программы, и поэтому оба метода имеют очень много общего. 38
СТРУКТУРНАЯ ИНДУКЦИЯ ДЛЯ НЕРЕКУРСИВНЫХ ПРОГРАММ Причем оказывается, что если программа по природе рекурсивна, то структуру данных очень просто использовать для выяснения процесса выполнения программы, и поэтому доказательство обычно легче проводить с помощью структурной индукции, а не индуктивных утверждений. Основная трудность в любом из методов – выбор правильных утверждений, которые связываются с точками в циклах программы, причем для разных методов эти утверждения различаются лишь в одном: индуктивные утверждения не должны содержать какой-либо информации об окончании работы, а утверждения для структурной индукции должны содержать информацию как о частичной правильности, так и об окончании. 39
«СОВРЕМЕННЫЕ» ИССЛЕДОВАНИЯ, СВЯЗАННЫЕ С ДОКАЗАТЕЛЬСТВОМ ПРАВИЛЬНОСТИ ПРОГРАММ В свое время в области доказательства правильности программ проводились интенсивные исследования. Для простоты обсужде- ния выделим среди этих исследований три основных направления: 1.Методы доказательства (частичной) правильности или конеч- ности. 2.Проблемы разработок программ и создания языков программи- рования. 3.Механизация процесса доказательства правильности. Эти направления перекрываются, можно лишь выявить характер исследований в каждом направлении и отметить некоторых из специалистов, которые работают в этих направлениях. Более подробно студенты могут ознакомления с тем или иным направлением исследований, работая самостоятельно. 40