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

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

F(Х) º IF Х = 1 THEN 1

ELSE OTHERWISE X•F(Х–1)

Чтобы понять, как работает такая программа, выполним ее для некоторого конкретного значения аргумента X. Например,

F(4) = 4 • F(3) [Так как условие 4 = 1 ложно, то F(4)=4•F(3).

Теперь нужно вычислить F(3), т. е. рекурсивно

обратиться к F.]

= 4 • 3 • F(2) [Т. к. при вычислении F(3) условие 3=1 ложно,

то F(3) = 3•F(2).]

= 4 • 3 • 2 • F(1) [Так как условие 2 = 1 ложно, то F(2) = 2•F(1).]

= 4 • 3 • 2 • 1 [Так как условие 1 = 1 истинно, то F(1) = 1.]

= 24 = 4 !

В разд. 4.2 мы докажем, что 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) = 1 + 1 = 2.]

= А(0, 3) [Так как X1 =0 истинно, следовательно,
А(0, 2) = 2 + 1 = 3.]

= 4 [Так как X1 = 0 истинно, следовательно,

А(0, 3) = 3 + 1=4.]

Из этого примера следует, что при выполнении вычислений для рекурсивной программы мы можем сталкиваться с неоднозначностями, которые требуют уточнений. Например, в приведенных вычислениях при обращении А(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) остается тем же, хотя последовательность вычислений отлична от предыдущей. Можно доказать, что если к одним и тем же аргументам некоторой рекурсивной функции применять две различные последовательности ее вычисления, то результат будет одним и тем же при условии конечности этих последовательностей. Однако вполне возможно, что одна последовательность не будет заканчиваться, хотя другая последовательность закончится. Рассмотрим следующий пример.

Пример 4.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))))) и т. д.

Таким образом, в первом случае последовательность вычислений F(1, 1) конечна и F(1, 1) = 0. Во втором случае вычисления не заканчиваются и, следовательно, значение F(1, 1) не определено. Однако отметим, что если для каких-либо аргументов в обоих случаях вычисления заканчиваются, то результат будет одним и тем же. Например, F(0, М) = 0 независимо от применяемых правил вычислений.

Итак, чтобы сделать наш язык программирования точным, нам нужно задать правила вычислений для программ, определяющие последовательность вычислений. В данной главе мы будем считать, что правило вычислений отдает предпочтение самому левому и самому внутреннему обращению. Другими словами, в любой из моментов вычислений первым начинает вычисляться левое и внутреннее обращение (для простоты далее везде будем опускать слово «самое») к функции F, все аргументы которой уже не содержат F. Это правило – не обязательно наилучшее, иногда оно может приводить к неоканчивающейся последовательности вычислений, хотя другое правило дало бы конечную последовательность (пример 4.3). Однако во многих существующих языках программирования используется правило вычислений, подобное описанному выше. Кроме того, как мы уже отмечали, если, следуя этому правилу, вычисления заканчиваются, то результат будет тем же, что и при других правилах, приводящих к окончанию. Большинство рассматриваемых нами программ заканчивается при любых значениях аргументов независимо от того, какие правила вычислений мы используем, а следовательно, и результат в любых случаях будет одинаковым. Однако для определенности все же будем считать, что предпочтение отдается левому внутреннему обращению.

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

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

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

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

CAR ( [А В С] ) дает А.

CAR ( [[А В] С] ) дает [А В].

CAR (NIL) не определено.

CAR (А) не определено.

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

CDR ( [А В С] ) дает [В С].

CDR ( [[А В] С] ) дает [С].

CDR ( [В] ) дает NIL (или [ ] ).

CDR (NIL) не определено.

CDR (А) не определено.

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

CONS ( А, [В С] ) дает [А В С].

CONS ( [А В], [В [С]] ) дает [[А В] В [С]].

CONS (А, NIL) дает [А].

CONS (А, В) не определено.

В некоторых из наших примеров мы будем использовать и специальные атомы ТRUЕ и FALSE.

Пример 4.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

Пример 4.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]

АРРЕND ([[А]], [В С] ) = СОNS ([А], АРРЕND (NIL, [В С])
= СОNS ([А], [В С])
= [[А] В С]

АРРЕND([А В], NIL) = СОNS (А, АРРЕND ([В], NIL))
= СОNS (А, СОNS (В, АРРЕND (NIL, NIL)))
= СОNS (А, СОNS ( [В] )
= СОNS (А, [В] )
= [А В]

В качестве упражнения проследите, как проходит процесс вычисления функции Аккермана (программа приведена в примере 4.2) при следующих аргументах а) А(1,1); б) А(2,1).

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

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

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

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