На этом шаге мы закончим рассмотрение примеров.

Пример 8. Рассмотрим рекурсивное определение, задающее функцию Аккермана:

  A(x₁,x₂) ⇔ IF x₁=0
              THEN x₂+1
              ELSE IF x₂=0
                     THEN A(x₁-1,1)
                     ELSE A(x₁-1,A(x₁,x₂-1)),

где х₁ и х₂ - неотрицательные целые числа.

Докажите, что вычисление значения функции А заканчивается для всех пар неотрицательных целых чисел (x₁,x₂).

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

Упорядочение зададим лексиграфическим порядком <, который определяется следующим образом:

  (х₁',x₂') < (x₁,x₂),

если и только если x₁' < x₁ или x₁'=x₁ & x₂' < x₂.

Докажем с помощью принципа трансфинитной индукции, что вычисление А для следующих пар неотрицательных чисел x₁ и x₂ заканчивается. Для этого необходимо доказать, что:
(1) А(х₁,х₂) заканчивается для наименьшего элемента вполне упорядоченного множества. Но наименьшим элементом является (0,0), и в этом случае вычисление А(0,0) заканчивается;
(2) для всех пар неотрицательных целых чисел (х₁,х₂)>(0,0): если вычисление значения А(х₁',х₂') заканчивается для любых (х₁',х₂')<(х₁,х₂), то заканчивается и вычисление значения А(х₁,х₂).

Предположение индукции. Пусть мы имеем некоторую пару (х₁,х₂) изнаем, что вычисление значения А(х₁',х₂') заканчивается для всех (х₁',х₂')<(х₁,х₂).

Если х₁ 0=0, то очевидно, что вычисление значения А(х₁,х₂) заканчивается. Если же х₁ ≠ 0 и х₂=0, то по индуктивному определению

   А(х₁,х₂)= А(х1-1,1).

Однако (х₁-1,1)<(х₁,х₂) и по предположению индукции вычисление значения А(х₁-1,1) заканчивается, а следовательно, заканчивается и вычисление значения А(х₁,х₂).

Если теперь х₁ ≠ 0 и х₂ ≠ 0, то

  А(х₁,х₂) = А(х₁-1, А(x₁,х₂-1)).

На следующем шаге вычислим А(х₁,х₂-1), но (х₁,х₂-1)<(х₁,х₂), и по предположению индукции вычисление А(х₁,х₂-1) должно закончиться.

После этого требуется вычислить значение А(х₁-1,z), где z - полученное значение А(x₁,x₂-1).

Каким бы ни было значение z, имеет место (x₁-1,z)<(x₁,x₂).

Следовательно, по предположению индукции заканчивается и вычисление А(x₁-1,z).

Итак, после вычисления значений А(х₁,х₂-1)=z и А(x₁-1,z) заканчивается вычисление значения А(х₁,х₂).

Отметим, что одновременно доказана завершаемость вычисления значений LISP-функции

   (DEFUN Akkerman (LAMBDA (M N)
      (COND ( (EQ M 0) (+ N 1) )
            ( (EQ N 0) (Akkerman (- M 1) 1) )
            (   T  (Akkerman (- M 1) (Akkerman M (- N 1))) ))
   ))

Пример 9. Рассмотрим рекурсивное определение функции, применимойк любому списку слов X и списку слов L:

   Member1(X,L) ⇔
         ⇔ IF L=NIL
           THEN FALSE
           ELSE IF X=CAR(L)
                  THEN TRUE
                  ELSE IF ATOM(CAR(L))
                         THEN Member1(X,CDR(L))
                         ELSE IF Member1(X,CAR(L))
                                THEN TRUE
                                ELSE OTHERWISE Member1(X,CDR(L)),

где TRUE (T - "истина"), FALSE (NIL - "ложь").

LISP-функция с эквивалентной семантикой такова:

   (DEFUN Member1 (LAMBDA (X L)
       (COND ( (NULL L) NIL )
             ( (EQ X (CAR L)) T )
             ( (ATOM (CAR L)) (Member1 X (CDR L)) )
             ( (Member1 X (CAR L)) T )
             (  T  (Member1 X (CDR L)) )
       )
   ))
   (RDS)

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

Превратите гипотезу в теорему.

Решение.

Предложение

Доказательство. Воспользуемся индукцией по общему числу n(L) вхождений скобок и атомов в список L.

Например, если список имеет следующее представление

  L ⇔ ((A B) C ((B A))),

то число скобок и атомов равно n(L)=13, а для списка

  CAR(L)=(A B)

число скобок и атомов равно n(L)=4.

Наименьшее из возможных значений общего числа скобок и атомов всписках достигается для пустого списка NIL=() и равно 2.

Пусть n(L)=2. Тогда L=NIL и

  Member1(X,L) = Member1(X,NIL) = Л (база индукции).

Докажем для всех n>2, что если значение функции Member1(X,L') вычисляется правильно для любого списка L' с общим числом скобок и атомов n'<n+1, то значение Member1(X,L) также будет правильно вычисляться для списка с общим числом скобок и атомов, равным n+1.

Предположим, что значение Member1(X,L') вычисляется правильно для любого списка L' c n'<n+1 (предположение индукции), а L - список, содержащий n+1 вхождение скобок и атомов.

Ясно, что L ≠ NIL, т.к. n+1>2 при n ≥ 2.

Если X=CAR(L), то Member1(X,L)=И, а это верно, ибо Х встречается в качестве элемента списка L.

Если Х=CAR(L) и ATOM(CAR(L))=И, то

  Member1(X,L) = Member1(X,CDR(L)).

Однако CDR(L) - список, содержащий n'<n+1 вхождений скобок и атомов. Поэтому по предположению индукции Member1(X,CDR(L)) правильно вычисляет значение И или Л в зависимости от того, входит Х или не входит в число элементов (любого уровня) списка CDR(L).

Так как X=CAR(L) и ATOM(CAR(L))=И, то мы знаем, что Х будет входить как элемент в L, если и только если Х входит как элемент в CDR(L).

Таким образом, в зависимости от того, входит или нет Х в число элементов L, мы будем получать верное значение.

Если X=CAR(L) и ATOM(CAR(L))=Л, Member1(X,CAR(L))=И, то

  Member1(X,L) = И,

что опять правильно, ибо известно, что в этом случае СAR(L) - список, содержащий n'<n+1 скобок и атомов. Из предположения индукции можно заключить, что значение Member1(X,CAR(L)) вычисляется правильно, и если Member1(X,CAR(L))=И, то Х действительно встречается в качестве элемента в CAR(L), а следовательно, и в L.

Наконец, если

  Х ≠ CAR(L), АТОМ(CAR(L)) = Л, Member1(X,CAR(L))=Л, то
  Member1(X,L) = Member1(X,CDR(L)).

Однако, т.к. CDR(L) - список с n'<n+1 вхождениями скобок и атомов, то из предположения индукции можно заключить, что функция Member1(X,CDR(L)) правильно вычисляет значения И или Л в зависимости от того, входит Х в число элементов CDR(L) или нет. А так как в этом случае X ≠ CAR(L) и ATOM(CAR(L))=Л, Member1(X,CAR(L))=Л, то Х будет элементом L, если и только если Х является элементом CDR(L).

Следовательно, и в этом случае значение

  Member1(X,L) = Member1(X,CDR(L)

будет вычисляться верно.

Предложение доказано.

Пример 10. Рассмотрим программу, которая применима к любым двум спискам L₁ и L₂, состоящих из целых чисел, расположенных в возрастающем порядке:

    IntOrd(L₁,L₂) ⇔
    ⇔ IF L₁=NIL
       THEN L₂
       ELSE IF L₂=NIL
              THEN L1
              ELSE IF CAR(L₁)<CAR(L₂)
                     THEN CONS(CAR(L₁),IntOrd(CDR(L₁),L₂)
                     ELSE IF CAR(L₂)<CAR(L₁)
                            THEN CONS(CAR(L₂),IntOrd(L₁,CDR(L₂))
                            ELSE OTHERWISE
                             CONS(CAR(L₁),
                             CONS(CAR(L₂),IntOrd(CDR(L₁),CDR(L₂))))

LISP-функция с эквивалентной семантикой такова:

   (DEFUN INTORD (LAMBDA (L1 L2)
      (COND ( (NULL L1) L2 )
            ( (NULL L2) L1 )
            ( (< (CAR L1) (CAR L2))
                 (CONS (CAR L1) (INTORD (CDR L1) L2)) )
            ( (< (CAR L2) (CAR L1))
                 (CONS (CAR L2) (INTORD L1 (CDR L2))) )
            ( T (CONS (CAR L1)
                      (CONS (CAR L2) (INTORD (CDR L1) (CDR L2))))))
   ))

Превратите гипотезу в теорему.

Решение.

Предложение. Для любых двух упорядоченных по возрастанию списков L₁ и L₂ результат вызова функции IntOrd(L₁,L₂) представляет собой упорядоченный по возрастанию список элементов, входящих в списки L₁ и L₂.

Доказательство. При рекурсивных обращениях к IntOrd() либо первый, либо второй, либо оба аргумента становятся проще. Поэтому естественно использовать принцип трансфинитной индукции по парам возможных длин (Len1,Len2) для списков L₁ и L₂ лексикографически упорядоченных с помощью "<".

Лексикографический порядок "<" определяется следующим образом:

   (Len1',Len2')<(Len1,Len2)

если и только если Len1'<Len1 или Len1'=Len1&Len2'<Len2.

Докажем для пары упорядоченных списков L₁ и L₂ с наименьшими длинами, что функция работает правильно. Но наименьшие длины есть (0,0), т.е. L₁ и L₂ - пустые списки. Следовательно, утверждение

  IntOrd(NIL,NIL)=NIL

верно (база индукции).

Докажем для всех пар длин (Len1,Len2)>(0,0), что если для всех списков L₁' и L₂', таких что

  (Len1',Len2')<(Len1,Len2),

правильно работает IntOrd(L₁',L₂') (предположение индукции), то правильно работает и IntOrd(L₁,L₂) (L₁ и L₂ имеют соответственно длины Len1 и Len2).

Предположим, что списки L₁ и L₂ являются такими, какие нам требуются, и предположение индукции верно. Легко проверить, что если либо L₁, либо L₂ есть NIL, то утверждение IntOrd(L₁,L₂)=NIL правильно. Поэтому будем предполагать, что L₁≠ NIL и L₂≠ NIL.

Возможен один из трёх случаев:

  (1) CAR(L₁)<CAR(L₂); 
  (2) CAR(L₁)>CAR(L₂);
  (3) CAR(L₁)=CAR(L₂).

Рассмотрим их последовательно.

(1) IntOrd(L₁,L₂) = IntOrd(CDR(L₁),L₂).

Однако длина CDR(L₁) меньше длины L₁, и, следовательно,

  (Длина CDR(L₁),Длина L₂)<(LENGHT1,LENGHT2)

из-за лексикографической упорядоченности.

Таким образом, применимо предположение индукции, и, следовательно, IntOrd(CDR(L₁),L₂) - действительно упорядоченный список всех чисел, входящих в качестве элементов и в CDR(L₁), и в L₂. Так как CAR(L₁)<CDR(L₂) и списки L₁, L₂ упорядочены, то, следовательно, CAR(L₁) не входит в список L₂. Отсюда вытекает, что упорядоченный список всех чисел, которые являются элементами как CDR(L₁), так и L₂, совпадает с упорядоченным списком всех чисел, которые являются элементами как L₁, так и L₂.

Следовательно, в этом случае утверждение

  IntOrd(L₁,L₂) = IntOrd(CDR(L₁),L₂)

справедливо.

(2) IntOrd(L₁,L₂) = IntOrd(L₁,CDR(L₂)).

Длина CDR(L₂) меньше длины L₂, и, следовательно,

  (Длина L₁,Длина CDR(L₂))<(Len1,Len2)

из-за лексикографического порядка. Поэтому к IntOrd(L₁,CDR(L₂)) применимо предположение индукции, и можно, используя соображения, аналогичные для случая (1), заключить, что и в этом случае

  IntOrd(L₁,L₂)

"работает" правильно.

(3) IntOrd(L₁,L₂) = CONS(CAR(L₁),IntOrd(CDR(L₁),CDR(L₂)).

Обе длины CDR(L₁) и CDR(L₂) меньше соответственно длин L1 и L2, и, следовательно, к IntOrd(CDR(L₁),CDR(L₂)) применимо предположение индукции. IntOrd(CDR(L₁),CDR(L₂)) представляет собой упорядоченный список всех чисел, которые входят как в CDR(L₁), так и в CDR(L₂). Кроме того, CAR(L₁)=CAR(L₂), и, следовательно CAR(L₁) (или CAR(L₂)) должен входить в качестве элемента в результирующий список.

Однако CONS(CAR(L₁),IntOrd(CDR(L₁),CDR(L₂))) состоит из

  IntOrd(CDR(L<SUB>1</SUB>),CDR(L<SUB>2</SUB>)),

содержащего в заданном порядке общие для CDR(L₁) и CDR(L₂) элементы, и одного дополнительного элемента CAR(L₁). Это именно тот список, который требуется, следовательно, в этом случае IntOrd() "работает" правильно.

Предложение доказано.

На следующем шаге мы приведем упражнения для самостоятельного решения.

Предыдущий шаг Содержание Следующий шаг