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

В качестве упражнения по данной теме попробуйте изменить приведенный в данном разделе принцип индукции для доказательства справедливости высказывания S(n) для целых чисел n, удовлетворяющих условию n ³ n0, а не только для любых положительных целых чисел.

1.2. Обобщенная индукция

Метод математической индукции можно обобщить и применять не только для доказательства высказываний о множестве положительных целых чисел, но и о более общих множествах некоторых объектов. Для этого сначала дадим определение, связанное с обобщением структуры целых чисел.

Определение. Говорят, что бинарное отношение < вполне упорядочивает множество X, или множество вполне упорядочено, если отношение < обладает следующими свойствами:

1) если x, y, z принадлежат X, а х < у и у < z, то х < z;

2) для х и у из X справедлива одна и только одна из трех возможностей: либо х < у, либо у < х, либо х = у;

3) если А – любое непустое подмножество X, то в А существует некоторый элемент х, такой, что х £ у для любого у, принадлежащего А.. Другими словами, любое непустое подмножество X содержит «наименьший элемент».

Отметим, что это определение касается обобщения структуры положительных (неотрицательных) целых чисел. Множество положительных целых чисел вполне упорядочено относительно обычного отношения <.

Пример 1.3. Множество всех целых не вполне упорядочено с помощью обычного отношения <. Такое множество обладает свойствами 1 и 2, но не обладает свойством 3. Множество всех отрицательных целых есть непустое подмножество множества целых, но не содержит наименьшего элемента.

Пример 1.4. Множество неотрицательных действительных чисел не является вполне упорядоченным с помощью обычного отношения <. Как и в предыдущем примере, для него выполняются свойства 1 и 2, но не выполняется свойство 3. Например, множество всех действительных чисел больше единицы, (такое множество можно обозначить следующим-образом: {х : х есть действительное и х > 1}) не содержит наименьшего элемента. Действительно, единица меньше любого элемента множества, но она множеству не принадлежит.

Пример 1.5. Множество всех упорядоченных пар неотрицательных целых чисел вполне упорядочено с помощью отношения лексикографического порядка <. Это отношение можно определить так: отношение (n1, n2) < (n3, n4) справедливо, если и только если (n1 < n3) или (n1 = n3 и n1 < n4). В качестве упражнения покажите, что такое отношение обеспечивает нужную упорядоченность.

Теперь сформулируем принцип обобщенной индукции для доказательства высказываний относительно любых вполне упорядоченных множеств.

Принцип обобщенной индукции

Пусть X – вполне упорядоченное относительно < множество, а S(х) – некоторое высказывание, касающееся элемента х из X. Если требуется доказать справедливость S(х) для всех х, принадлежащих X, то необходимо:

1) доказать, что справедливо S(х0), где х0 – наименьший элемент в X;

2) доказать для всех х в X, удовлетворяющих условию х0 < х, что если справедливо S (у) для всех у < х, то справедливо и S(х).

Отметим, что если X – множество положительных целых чисел, а отношение < имеет обычный смысл, то принцип обобщенной индукции идентичен принципу строгой индукции (разд. 1.1).

Чтобы убедиться в действенности принципа обобщенной индукции как метода доказательства, предположим, что S(х) – некоторое высказывание, для которого уже доказаны оба положения. Мы хотим сделать вывод о том, что S(х) справедливо для любых х в X. Предположим, что это не так. Пусть множество А = {х: х принадлежит X и S(х) ложно}. Если S(х) не справедливо для всех х в X, то А – непустое подмножество X. Так как X вполне упорядочено, то известно, что А содержит наименьший элемент а0. По определению это наименьший элемент X, для которого S(х) не справедливо, Таким образом, S(у) справедливо для всех у (если они есть), удовлетворяющих условию у < а0. Если а0 – наименьший элемент в X, то S(а0) справедливо, что следует из первого положения. В противном случае из справедливости S(у) для всех у < а0 и второго положения вытекает, что S(а0) справедливо. Но это противоречит предположению, что а0 принадлежит А и S(а0) ложно. Единственный способ устранить это противоречие – считать А пустым множеством, т. е. в X нет элементов, для которых высказывание S(х) ложно.

Пример 1.6. Рассмотрим последовательность чисел, определенную следу­ющим образом: S0, 0 = 0, а для любой другой пары неотрицательных чисел m, n

Например, первые элементы этой последовательности:

S0, 0 = 0, S1, 0 = S0, 0 + 1 = 0 + 1 = 1,

S0, 1 = S0, 0 + 1 = 1, S1, 1 = S1, 0 + 1 = 1 + 1 = 2,

S2, 0 = S1, 0 + 1 = 2, S2, 1 = S2, 0 + 1 = 3, ... .

Нужно доказать, что Sm, n = m + n для любых неотрицательных целых m, n. Используем принцип обобщенной индукции на множестве X упорядоченных пар неотрицательных целых чисел. Множество упорядочено на основе лексикографического порядка, описанного в примере 3. Чтобы доказать справедливость Sm, n = m + n для любых < m, n > в X, необходимо:

1) доказать, что Sm, n = m + n справедливо, если < m, n > – наименьший элемент в X. Но так как наименьший элемент – пара < 0, 0 >, то нужно показать, что S0, 0 = 0 + 0 = 0. Это очевидно по определению S0, 0;

2) доказать, что если Sm’, n’ = m’ + n’ справедливо для любых пар < m’, n’ > < < m, n >, то справедливо и Sm, n = m + n для любых < 0, 0 > < < m, n > в X. Предположим, что формула Sm’, n’ = m’ + n’ верна для < m’, n’ > < < m, n >. Это гипотеза индукции. Нужно показать, что Sm, n = m + n. Существует две возможности: либо
n = 0, либо n ¹ 0. Если n = 0, то по определению Sm, n = Sm–1, n + 1. Однако < m–1, n > < < m, n >, и, следовательно, по нашей гипотезе Sm–1, n  = (m – 1) + n. Поэтому Sm, n = Sm–1, n+ 1 = = (m – 1 + n) + 1 =
= m + n. Если n ¹ 0, то Sm, n = Sm, n–1 + 1 по определению. Но
< m, n–1 > < < m, n > и по гипотезе Sm, n–1 = m + (n – 1). Следовательно, в этом случае Sm, n = Sm, n–1 + 1 = (m + n – 1) + 1 = m + n, что и требовалось доказать.

Глава 2. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ

В первой части конспекта лекций мы сформулировали и показали на примерах, как используется метод индуктивных утверждений. И формулировки индуктивных утверждений, и процесс доказательства проводились довольно неформальным образом. Если использовать какую-либо формальную нотацию для записи индуктивных утверждений и соответствующую дедуктивную систему для проведения доказательств, то можно формализовать весь этот процесс. В данной главе мы обсудим некоторые аспекты такой формализации. Если мы надеемся, что в конце концов придем к тому, что при поддержке некоторой «механической» системы будем либо выполнять доказательство, либо его проверять, то некоторого типа формализация нам необходима. Студенты, которых интересует вопрос формализации, могут обратиться к литературе [3, 4, 5]. Наиболее изученной формальной нотацией для формулирования и проведения математического доказательства является исчисление предикатов. Мы полагаем, что студент знаком с такого рода нотацией, либо предлагаем ему воспользоваться книгами по математической логике [7, 8] и самостоятельно ознакомиться с данными вопросами.

Напомним, что метод индуктивных утверждений состоит в следующем [1]. Для доказательства частичной правильности некоторой блок-схемы относительно утверждений А и С мы связываем утверждение А с начальной точкой блок-схемы, а утверждение С – с конечной. Кроме этого, необходимо выделить и связать с блок-схемой некоторые другие утверждения (описывающие отношения между значениями переменных, справедливые в момент попадания в соответствующую точку программы). Нужно, в частности, связать по крайней мере с одной из точек в замкнутом пути (цикле) одно такое утверждение. Затем необходимо для каждого пути в блок-схеме, ведущего из точки i с утверждением Аi в точку j с утверждение Аj при условии, что на пути из i в j нет промежуточных точек с утверждениями, доказать, что если мы находимся в точке i и справедливо утверждение Аi а затем переходим по нашему пути в точку j, то при попадании в эту точку будет справедливо утверждение Аj. Для формализации такого доказательства необходимо: