6.1.9 Метод структурной индукции

Обычно рекурсивная подпрограмма предполагает разложение класса всех задач, решаемых данной подпрограммой, на совокупность подзадач таким образом, что любые две подзадачи либо не пересекаются, либо одна из них является подзадачей другой. При этом описание подпрограммы строится по следующей схеме: сначала в ней определяется споcоб решения тривиальных случаев (наипростейших подзадач), каждый из которых может быть разрешен непосредственно (без рекурсивного вызова), а затем -- способ вычисления результата для общего случая, причем используется сведение к решению одной или нескольких более простых подзадач (через рекурсивные обращения к той же подпрограмме).

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

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

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

Проиллюстрируем применение метода для доказательства того, что рекурсивная функция ФАКТ(N) вычисляет факториал N! заданного неотрицательного целого числа N.

Базис тривиален: при N = 1 имеем ФАКТ(N) = 1 = 1!.

Для доказательства индуктивного перехода рассмотрим такое целое N, что N $>$ 1 и ФАКТ(М) = М! для всех М, 1$\leq$ M $<$ N. Тогда в соответствии с определением получаем

ФАКТ (N)=N$\ast$ ФАКТ(N-1)= N$\ast$(N-1)!)=N!,

что завершает доказательство правильности функции ФАКТ.

Рассмотрим функцию, известную как функция Аккермана:

procedure A (N:integer; M:integer):integer;
begin (* {N $\geq$ 0, M $\geq$ 0} *)
    if N = 0 then A := M+1 elsif M = 0 then A := A(N-1,1) else A := A(N-1, A(N,M-1)) end
end A.

Для нее, в частности, имеем А(1,2) = А(0,А(1,1)) = А(0,А(0,А(1,0))) = А(0,А(0,А(0,1))) = А(0,А(0,2)) = А(0,3) = 4.

Методом структурной индукции покажем, что А(N,M) заканчивается для любой пары неотрицательных целых чисел N и M.

Будем рассматривать подзадачи, каждая из которых определяется некоторой парой неотрицательных чисел K и R и представляет собой вычисление функции A для всех таких пар (X,Y), что либо X $<$ K, либо X = K и Y $\leq$ R.

Таким образом, A(K,R) является подзадачей A(N,M), если K $<$ N, либо K = N и R $\leq$ M, и наипростейший случай-- это A(0,0).

Ясно, что вычисление A(0,0) заканчивается.

Пусть N и M не равны нулю одновременно, и пусть A(X,Y) заканчивается для всех таких X и Y, что либо X $<$ N, либо X = N и Y $\leq$ M. Рассмотрим A(N,M). Если N = 0, то очевидно, что A(N,M) закончится. Если N $\neq$ 0 и M=0, то A(N,M) = A(N-1,1) и по гипотезе индукции вычисление A(N-1,1) закончится, а следовательно, закончится и вычисление A(N,M). Пусть N $\neq$ 0 и M $\neq$ 0, тогда A(N,M) = A(N-1, A(N,M-1)) и, дважды применяя индуктивное предположение, сначала получаем завершимость A(N,M-1), а затем завершимость A(N-1,K), где K = A(N,M-1).

В качестве последнего примера рассмотрим следующую функцию, известную как функция 91 Маккарти:

procedure F (N:integer):integer;
begin if N $>$ 100 then F := N-10 else F := F(F(N+11)) end end F;

и докажем, что F(N) = 91 для всех N $\leq$ 100.

Базис (при N=100) очевиден: F(100)=F(F(111))=F(101)=91.

Пусть N $<$ 100 и для любого такого M, что 100$\geq$ M $>$ N, выполняется F(M) = 91. Для нахождения значения F(N) отдельно рассмотрим два случая: 89$<$ N$<$100 и N $\leq$ 89. При 89 $<$ N $<$ 100 имеем F(N)=F(F(N+11))=F((N+11)-10) = F(N+1)= (по индуктивному предположению)= 91. Пусть N $\leq$ 89, тогда F(N)=F(F(N+11)) = (по индуктивному предположению)= F(91)= (по индуктивному предположению)= 91.

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