Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

19.4. ТЕОРЕМА О ВЕРИФИКАЦИИ

481

Схематически его можно описать следующим образом. Выходные

переменные объявляются действующими. Далее идем по графу вывода

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

которая нужна для получения действующих частей заключения. После

того, как прошли по выводу, возвращаемся вниз и пересчитываем ти-

пы, соответствующие формулам, с учетом лишь действующих их ком-

понент.

Более того, призрачными могут быть целые типы данных. Напри-

мер, оценки, используемые в доказательствах завершаемости циклов,

могут принадлежать некоторому абстрактному множеству, даже более

общему, чем множество ординалов, скажем, до

, и задаваться вопро-

сом о реализации данного множества не нужно.

§ 19.4. ТЕОРЕМА О ВЕРИФИКАЦИИ

Рассмотрим следующую задачу, которая часто ставится теоретиками и

практиками для программирования.

Дана программа, доказать ее правильность.

Содержательный анализ этой задачи сразу же выявляет некоторые по-

дозрительные места. Если уже дана программа и она работает, то зачем

же доказывать ее правильность? Если же еще нет уверенности в том,

всегда ли она работает, не разумнее ли было бы поставить задачу попы-

таться найти слабые места в данной программе? Далее, своевременно ли

ставится эта задача, может быть, разумнее было бы ставить ее не

тогда, когда программа уже дана, а тогда, когда она еще создается?

Словом,при получении такой задачи невольно закрадывается мысль,

что в данном случае скорее нужно было бы не доказательство, а закли-

нание либо молитва, дабы освятить уже готовое решение.

Анализ положения дел в данной области подтверждает подозрения.

Конечно же, были случаи, когда программу доказывали, после чего в

ней находили ошибку. Конечно же, теоретические системы доказатель-

ства правильности программ не работали почти ни в одном практически

пригодном случае. А если где-то и работали, немедленно отказывались

работать при малейших расширениях либо видоизменениях класса про-

грамм

Если же отходить от требований строгости, то получаемую конструкцию доказатель-

ством нельзя называть. Предложение не может быть на 80% доказанным, как и женщи-

482

ГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ

Но такие признаки еще не доказывают наличия принципиальных

слабостей в постановке задачи, хотя и делают это вероятным. Нужно

вернуться к теоретическому анализу на другом уровне.

Несмотря на все опасности слишком позитивной постановки задачи,

проблема доказательства правильности программ была бы полностью

оправдана, если бы удалось установить, что сложность поиска доказа-

тельства, опирающегося на уже известный текст программы, меньше,

чем поиск его с самого начала, параллельно с построением программы.

Тогда бы было ясно, что игра в принципе стоит свеч.

Но, применяя установленный в предыдущих параграфах гомомор-

физм доказательств в программы, можно увидеть, что это не так.

Пусть программа должна построить по входным данным,удовлетво-

ряющим условию

A(x), и выходные, удовлетворяющие условию

B(x, y)

Теорема 19.1. Доказательство правильности программы с увеличени-

ем длины не более чем в 3 раза перестраивается в конструктивное до-

казательство, из которого извлекается программа для решения той

же задачи.

Заметим, что если теоретическая оценка увеличения длины вывода

столь низка, то практически это чаще всего означает на самом деле его

укорочение.

Итак, теоретический анализ подтверждает тот практический вывод,

что восстановить обоснование уже готовой программы во всяком случае

не легче, чем написать его, пока она еще развивается.

на не может быть на 80% беременна. Даже видные математики при первых попытках

применения компьютера для доказательства теорем часто попадали в данную ловушку,

сочтя, что громадный перебор может послужить основой, чтобы оставить некоторые

случаи недоказанными. Но, как правило, быстро находились контрпримеры, выпавшие

из перебора.

Мы рассматриваем случай лишь одной входной и выходной переменной, посколь-

ку адекватной формализацией, сохраняющей гомоморфизм между доказательствами и

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

есть прямые произведения и прямые суммы, позволяющие свести несколько альтерна-

тивных наборов входных (выходных) данных в одну переменную.

19.5. СТРУКТУРНЫЕ ЗАВЕРШИТЕЛИ

483

§ 19.5. ПРОБЛЕМА СОВМЕСТИМОСТИ ОПЕРАТОРОВ

НА ПРИМЕРЕ EXIT

Известно, что с внешней стороны переход к структурному программи-

рованию выглядит как изгнание операторов перехода. Но полностью из-

гнать их не удается, и поэтому возникает понятие структурного перехо-

да, который не затемняет структуру программы, а, наоборот, делает ее

прозрачнее.

Общая черта таких структурных переходов состоит в том, что они

идут вперед и выводят нас из программной структуры, которая сделала

свое дело, но не может быть завершена по формальным мотивам.

Например, при поиске информации мы можем войти в целую после-

довательность операторов и процедур поиска, но, когда нужная инфор-

мация найдена, все они немедленно становятся лишними и мы должны

перейти в самую внешнюю процедуру, к обработке найденной инфор-

мации.

Средства, предлагаемые в данном случае чистым структурным про-

граммированием, несколько неуклюжи. Предлагается завести логиче-

скую переменную, скажем,

found

, которая устанавливается в

true

при

успешном поиске, и во всех разумных местах писать вместо

нечто

вроде

if found then S ﬁ

;

Поэтому намного естественней выглядит возможность выйти из внеш-

ней процедуры оператором типа

exit(f)

Данный оператор выглядит весьма естественно, и здесь длительное

время не возникало даже тени сомнения, совместим ли он со структур-

ным программированием. Завершители стали добавляться практически

везде. И лишь его логический анализ выявил, что не все так просто, и

показал корни некоторых редких, но вредных ошибок в системах про-

граммирования высокого уровня.

Итак, структурный переход связан с достижением цели более вы-

сокого ранга в процессе стремления к некоторой подцели. Попытаемся

формализовать его логически. В естественном выводе такую ситуацию

можно описать следующим образом. Мы находились внутри вложенно-

го вспомогательного вывода, а доказали цель объемлющего. Такая си-

туация в графе вывода описывается новым структурным правилом —

правилом приятной неожиданности, разрешающим завершать все вло-

женые друг в друга вспомогательные выводы, если во внутреннем до-

казана цель самого внешнего. Рассмотрим детальнее выводы с таким

484

ГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ

правилом.Для простоты ограничимся пропозициональной логикой, тем

более что принципиальные выводы она уже позволяет увидеть.

Предложение 19.5.1. Правило приятной неожиданности допустимо в

классической логике.

Доказательство. В самом деле, рассмотрим последовательность вло-

женных вспомогательных выводов

, ..., Σ

, допущением самого

внешнего из которых является A

, а ожидаемым результатом — B

, и

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

, а цель — B

Пусть во внутреннем выводе доказано

. Тогда мы можем доказать

в непосредственно объемлющем его выводе вместо получаемой из не-

го формулы C

n−1

формулу C

n−1

∨ A

. В самом деле, рассмотрим все

четыре косвенных правила классической логики.

Пусть

используется в правиле приведения к абсурду. Тогда за-

меним это правило на правило дедукции и получим A

⇒ B

. Вос-

пользовавшись классической эквивалентностью, получаем

∨ B

Правило от противного рассматривается точно так же.

Пусть теперь

используется в правиле разбора случаев. Тогда при-

соединяем к получившейся совокупности случаев еще один случай B

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

используется правилом дедукции, получаем

⇒ B

∨ B

и по классической тавтологии — (A

⇒ B

) ∨ B

Во всех промежуточных выводах вместо

разбором случаев полу-

чаем C

∨ B

Таким образом, протягиваем результат во внешний вспомогатель-

ный вывод

Заметим, что процедура устранения приятной неожиданности очень

напоминает описанную выше процедуру устранения стуктурного завер-

шителя в программировании. Заметим также, что она интенсивно поль-

зуется сугубо классическими тавтологиями.

Предложение 19.5.2. Правило приятной неожиданности превращает

интуиционистскую логику в классическую.

Доказательство. Больше, чем в классическую, превратить оно не мо-

жет, по предыдущему результату. Значит, достаточно вывести одну из

формул,из которых следует закон исключенного третьего. Выведем фор-

19.5. СТРУКТУРНЫЕ ЗАВЕРШИТЕЛИ

485

мулу Пирса.

∗ (A ⇒ B) ⇒ A



∗ A

Допущение и одновременно приятная неожиданность



Цель, которая никому уже не нужна

A ⇒ B

A цель подвывода

((A ⇒ B) ⇒ A) ⇒ A

Из доказанной формулы, как известно,следует закон исключенного тре-

тьего.

Теперь проанализируем возникшие сложности. Пронос приятной не-

ожиданности сквозь дизъюнкцию ничему не мешает. Вынос ее из им-

пликации уже вреден. Столь же плох и вынос из доказательства приве-

дением к абсурду, но эти части вывода никогда в программу не пере-

ходят. Итак, плохо выходить структурно из вызовов процедур, причем

таких, которые являются параметрами других процедур.

Дополнительные рассмотрения с кванторами и индукцией только

подтверждают этот вывод. А поскольку функционалы высших типов

в программировании использовались редко и плохо, эта дополнитель-

ная ошибка оставалась укрытой. Ведь структурные выходы из разборов

случаев и циклов ничему не мешают, и даже из последовательности вы-

зовов процедур, ни одна из которых не передана в качестве параметра

другой процедуре, можно также выйти безопасно.

Более того, алгоритмическими средствами установить случаи не-

корректности структурного завершителя невозможно, поскольку интер-

претатор соответствующих теоретических конструкций пишется момен-

тально. Разваливается структура утверждений о программе, но кого это

интересует в алгоритмическом подходе, лишь бы программа исполня-

лась.

Литература

[1] Аристотель. Первая аналитика.Сочинения,т. 1, М.: Мысль, 1975,

с. 117–254.

[2] Аристотель. Вторая аналитика. Сочинения, т. 1, М.: Мысль,

1975, с. 255–346.

[3] Аристотель. Категории. Сочинения, т. 2, М.: Мысль, 1978, с. 51–

90.

[4] Аристотель. Метафизика. Сочинения, т. 1, М.: Мысль, 1975.

[5] Аристотель. Об истолковании. Сочинения, т. 1, М.: Мысль, 1975,

с. 91–116.

[6] Аристотель. О софистических опровержениях. Сочинения, т. 1,

М.: Мысль, 1975, с. 533–593.

[7] Аристотель. Топика.Сочинения,т. 1, М.: Мысль, 1975, с. 347–532.

[8] Дж. Булос, Р. Джеффри. Вычислимость и логика. М., Мир, 1994.

[9] Дж. Вейценбаум. Возможности вычислительных машин и чело-

веческий разум. М.: Радио и связь, 1982.

[10] В. И. Вернадский. Труды по всеобщей истории науки. М.: Наука,

1988.

[11] П. Вопенка. Математика в альтернативной теории множеств.

М.: Мир, 1983.

[12] Р. Голдблатт. Топосы. Категорный анализ логики. М.: Мир, 1983.

[13] Р. Голдблатт. Логика времени и вычислимости. М.: ОИЛКРЛ,

1992.

486

ЛИТЕРАТУРА

487

[14] С. С. Гончаров, Ю. Л. Ершов, К. Ф. Самохвалов. Введение в логику

и методологию науки. М.: Интерпракс, 1994.

[15] М. Девис. Прикладной нестандартный анализ. М.: Мир, 1980.

[16] Ю. Л. Ершов. Теория нумераций. М.: Наука, 1977.

[17] В. Г. Кановей. Аксиома выбора и аксиома детерминированности.

М.: Наука, 1984.

[18] Н.И. Конрад. У-цзы.Трактат о военном искусстве.Перевод и ис-

следование. в кн.: Н. И. Конрад. Избранные труды. Синология.М.,

1977.

[19] М. Крейнович. Из чего следует закон исключенного третьего?

Тр. научных семинаров ЛОМИ, вып. 52 (1978), с. 132–145.

[20] К. Куратовский, А. Мостовский. Теория множеств. М.: Мир,

1970.

[21] Л. Кэрролл. История с узелками. М.: Мир, 1973.

[22] Н.Н. Непейвода.О формализации неформализуемых понятий:ав-

топродуктивные системы теорий. Семиотика и информатика,

вып. 25 (1985), с. 46–93.

[23] Омар Хайям в кругу мудрости. Симферополь: Реноме, 1999

[24] К. М. Подниекс. Вокруг теоремы Г

еделя. Рига: 1981.

[25] И. Пригожин. От существующего к возникающему. М.: Наука,

1985.

[26] Е. Рас

ева, Р. Сикорский. Математика метаматематики. М.: На-

ука, 1972.

[27] С. П. Расторгуев, В. Н. Чибисов. Цель как криптограмма. М.:

Яхтсмен, 1996.

[28] Р. Р. Столл. Множества. Логика. Аксиоматические теории. М.:

Просвещение, 1968.

[29] В. А. Успенский. Что такое нестандартный анализ? М.: Наука,

1987.

488

ЛИТЕРАТУРА

[30] П. Тейяр де Шарден. Феномен человека. М.: Наука, 1987.

[31] А. Т. Фоменко. Глобальная хронология. М.: МГУ, 1993.

[32] Chin-lang Cheng, R. Lee. Symbolic logic and mechanical theorem

proving. Academic Press, 1973 (русский перевод: Ч. Чень, Р. Ли.

Математическая логика и автоматическое доказательство теорем.

М.: Наука, 1983).

[33] H. B. Curry. Towards authomatical program construction, Proc.

NATO Conf. on Automatic Computing, Paris, 1952, p. 35–64.

[34] H. B. Curry, R. Howard. Combinatory logic, vol. 2, Addison, 1968.

[35] S.C. Kleene.Introduction in metamathematics. New-York: 1952 (рус-

ский перевод С. К. Клини. Введение в метаматематику. М.:

1957).

Предметный указатель

Symbols

n-ка, 84

Art, ix

Craftsmanship, ix

Currying , см. Преобразование Кар-

ри

Hypercriticism, ix

Knowledge

formal, viii

informal, viii

Mastery, viii

Mathematician, viii

Notion, x

Science, viii

Term

in common language, x

Адекватный, xvi

Аксиома

Архимеда, 262

выбора, 102, 106, 110, 278

детерминированности, 281

зависимого выбора, 280

композиций, 343

перечислимости, 347

рекурсивного определения, 345

универсального алгоритма,342

Аксиома

подстановки, 109

Алгебра

Линденбаума-Тарского, 201

интуиционистская, 430

булева, 200, 410

гейтингова, 431

псевдобулева, 431

Алгоритм

британского музея, 338

экстенсиональный, 348

Алфавит, 133

Антиизоморфизм, 462

Арифметика Пеано, 353

Атом, 319

Бесконечный спуск, 142

Буддизм, 450

Возврат (backtracking), 326

Вселенная, xxi

Вывод, 225

вспомогательный, 290

естественный, 303

незаконченный, 308

489

490

ПРЕДМЕТНЫЙ УКАЗАТЕЛЬ

подвывод, 290

Выражение

замкнутое, 183

Выражения

типизированные, 172

Высказывание, 15

Квазивысказывания, 18

интенсиональное, 60

общее, 16

сложное, 17

точно сформулированное, 6

экстенсиональное, 60

Гербалайф, xx

Герменевтика, xii

Гностицизм, 450

Граф, 120–125

Квазиграф, 123

Орграф, 124

Псевдограф, 123

неориентированный, 124

ориентированный, 124

оснащенный, 124

Двойственность, 126

аргументов и функций, 382

Дерево, 121

Веер, 147

нагруженное, 145

с конечными путями, 145

Диаграмма

Венна, 77–82

Гессе, 94

Эйлера, 76–82

коммутативная, 125–133

Дизъюнкт, 319

хорновский, 325

Доказательство, 403

от противного, 294

Задача

конструктивная, 412

математическая, 404

Закон

Тезис Черча, 350

алгебраический, 399–400

достаточного основания, 398

исключенного третьего,295,398

сильный, 398, 424, 425

непротиворечия, 395

сокращенный, 396

тождества, 394

Значение

в интерпретации, 189

истинностное, 21

логическое, 21

Идеи, xxi

Идентификатор, 134

Индукция

bar-индукция, 147

возвратная, 140–142

математическая, 137–140

по построению, 144

трансфинитная, 149–163

Интеллект

искусственный (ИИ), 18

Интерпретация, 189, 191

колмогоровская, 422

обеднение, 196

обогащение, 196

подинтерпретация, 196

расширение, 196

Интуиционизм, 413

Ипостась, 373

Истинность

по Тарскому, 339

Исчисление, 224

Кавычки, xxvi

Категория, 127–133

морфизмов, 129

объект, 127