О математической индукции
Я особо выделил математическую индукцию потому, что это единственный способ рассуждения, который в конечном итоге позволяет нам совладать с циклами (типа тех, что описываются с помощью заголовков повторения) и с рекурсивными процедурами. Хочу привести один пример.
Рассмотрим последовательность значений d0, d1, d2,d3, ...
заданную так:
для i=0 di=D (2a)
для i>0 di = f(di-1) (2b)
где D - некое заданное значение и f - заданная (вычислимая) функция. Требуется присвоить переменной d значение первого элемента dk из последовательности, которое удовлетворяет заданному (вычислимому) условию "утв". Известно, что такое значение существует для конечного k. Более формально можно сказать, что требуется установить отношение
d=dk (3)
где k задается выражениями
утв(dk) (4)
и
non утв (di) (5)
для всех i, удовлетворяющих 0 i < k
Рассмотрим теперь следующий фрагмент программы:
| d:=D
while non утв (d) do d:=f(d) |
(6) |
Здесь первая строка представляет начальную установку, а вторая представляет цикл, управляемый (надеюсь, не требующим пояснений) заголовком повторения while ... do. (С помощью условия if ... do, использованного в предыдущем примере, семантика заголовка повторения может быть описана формально: текст
while B do S
семантически эквивалентен тексту
if B do
begin S; while B do S end
и означает, что non В - необходимое и достаточное условие прекращения повторений.)
Мы будем называть в конструкции while B do S оператор S "повторяемым оператором" и докажем, что в программе (6) после n-го выполнения повторяемого оператора справедливо (при n0)
d=dn (7а)
и
non утв (di) для всех значений i, удовлетворяющих 0i<n (7b)
Методом перечисления убеждаемся в том, что это утверждение справедливо при n=0; мы хотим доказать (также методом перечисления), что если оно справедливо при n=N (N0), то оно справедливо и при n=N+1.
После N-го выполнения повторяемого оператора отношения (7a) и (7b) выполняются при n=N. Для того чтобы произошло (N+1)-е выполнение, необходима и достаточна истинность условия
non утв (d)
которое в силу (7а) для n=N (т. е. при d=dN) означает
non утв (dN)
Поэтому условие (7b) справедливо для n=N+1. Кроме того, из равенства d=dN и из (2b) следует, что
f(d)=dN+1
так что непосредственным результатом (N+1)-го выполнения повторяемого оператора будет установление отношения
d:=f(d)
т. е. отношения (7а) для N=N+1, и таким образом индуктивный переход (7) обоснован.
Теперь покажем, что повторения прекращаются после k-гo выполнения повторяемого оператора. При n>k не может быть n-го выполнения, так как в силу (7b) это означало бы
non утв (dk)
а это противоречило бы условию (4).
Если повторения прекращаются после n-ro выполнения повторяемого оператора, то необходимое и достаточное условие прекращения повторений, т.е.
non(non утв (d))
в силу (7а) принимает вид
утв (dn) (8)
Этим исключается прекращение повторений при n<k, так как оно противоречило бы условию (5). Итак, повторения прекратятся при n=k, и поэтому (3) следует из (7а), (4) следует из (8) и (5) - из (7b). Наше доказательство завершено.
Прежде чем отвлечься от этого примера, иллюстрирующего применение математической индукции в рассуждениях, я хочу сделать несколько дополнительных замечаний, потому что предчувствую, что к этому времени некоторые мои читатели (особенно опытные и компетентные программисты) придут в негодование; речь идет о тех читателях, для которых правильность программы (6) настолько очевидна, что их удивляет вся эта суета: "К чему напыщенное сведение проблемы к условиям (3), (4) и (5), когда всякий знает, что собой представляет первое значение из последовательности, удовлетворяющее некоему условию? Разумеется, он не может ожидать, что мы - люди, загруженные работой,- будем предоставлять такие длинные доказательства с полной математической отделкой всякий раз, когда употребим такой простой цикл, как этот." И так далее ...
Признаюсь чистосердечно: пышность и пространность приведенного выше доказательства раздражают и меня. Однако в настоящее время у меня нет лучшего выхода, если я действительно стремлюсь обосновать правильность этой программы. Впрочем, иногда это вызывает у меня такую же злость, какую я испытывал много лет назад, изучая мудреные доказательства первых простых теорем планиметрии, в которых утверждались факты, не менее очевидные, чeм сами аксиомы Евклида.
Конечно, я не осмеливаюсь утверждать (по крайней мере теперь!), что программист должен предоставлять такое доказательство всякий раз, когда пишет в своей программе простой цикл. Тогда бы он вообще никогда не смог написать программу любого размера! ЭТО было бы столь же нереально, как явное и полное сведение любого доказательства в планиметрии к аксиомам Евклида. (См. раздел "О количественной ограниченности наших возможностей".)
Хочу сделать три вывода из сказанного. Во-первых, когда программист рассматривает конструкцию типа (6) как заведомо правильную, он имеет на это право потому, что знаком с такой конструкцией. Я предпочитаю рассматривать его поведение как неосознанную ссылку на теорему, которую он знает, хотя не исключено, что он никогда не удосуживался сформулировать ее. Когда-то он убедился в ее правильности, хотя, возможно, он уже забыл свой способ доказательства и хотя этот способ (возможно) и непригоден для публикации. Тем не менее мы могли бы сформулировать свое мнение о программе (6) в виде, скажем, "теоремы линейного поиска", а зная такое название, гораздо легче (и более естественно) апеллировать к нему интуитивно.
Во-вторых, насколько мне известно, не существует набора теорем типа рассмотренной выше, полезность которых была бы общепризнанной. Однако не следует удивляться этому, так как отсутствие такого набора теорем является непосредственным следствием того факта, что не сформулировано четко понятие основного объекта, т.е. программы. Тип объекта, с которым имеет дело программист, т.е.
программы, значительно менее формализован, чем тип объекта в планиметрии. Между тем развитая интуиция программиста выражается, по-видимому, в том, что он ограничивается по мере возможности хорошо знакомыми структурами программ и проявляет особую осторожность и тщательность при построении необычных (для себя) программных конструкций. Однако для формализации программирования могли бы оказаться полезными поиски теорем, соответствующих таким необычным программам.
В-третьих, протяженность доказательства, которое потребовалось нам в предыдущем примере, представляет собой предостережение, которое не может быть оставлено без внимания. Конечно, не исключено, что более искусный математик провел бы доказательство короче и изящнее, чем это удалось мне. Лично же я склонен сделать вывод, что само программирование труднее, чем принято считать. Будем смиренно воспринимать громоздкость доказательства как убедительный совет ограничиваться по возможности простыми структурами и проявлять максимальную интеллектуальную умеренность, остерегаясь "хитроумных конструкций" как чумы.
