[ «Прикладная логика Учебное пособие Рекомендовано Государственным комитетом Российской Федерации по высшему образованию в качестве учебного пособия для студентов высших учебных заведений, обучающихся по специальностям ...»
16.1.4. Разногласия и новые идеи А в самом интуиционизме начались расхождения. Многие были недовольны формализацией отрицания по Гейтингу и начали ее варьировать (минимальная логика, сильное отрицание, безотрицательная математика). Другие начали проявлять недовольство слишком сильными, по их мнению, абстракциями, введенными Брауэром, особенно это течение усилилось после появления точного понятия алгоритма. Третьи... но в учебнике можно и остановиться.
ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА
Реакция Брауэра была совершенно неординарной для отца-основателя школы. Вместо обвинений в адрес ревизионистов и уклонистов он спокойно сказал:Поскольку интуиционисты говорят на неформализованном языке, среди них должны были появиться разногласия.
Там, где есть единомыслие, нет мысли! Если бы побольше выдающихся умов это понимали, и понимали бы еще, насколько апостолы, как правило, профанируют и компрометируют идею!
Принципиальный плюрализм и уважение к чужой точке зрения у Брауэра тем более примечательны, что в жизни он отдал дань традиционной слабости творческих людей, часто позволявших себя соблазнить лозунгами экстремистских групп. Брауэр поддерживал Гитлера до тех пор, пока не столкнулся с гитлеризмом на практике, пока Германия не оккупировала самым подлым и вероломным образом нейтральную Голландию. Брауэр после этого занял патриотическую позицию.
После войны Брауэр опубликовал серию работ, в которых как будто задался целью показать, что он не хуже других умеет создавать альтернативы. Он ввел в математику последовательности, зависящие от развития самого математического знания (и тем самым в дальнейшем, через своего ученика Бета, дал начало новой теории моделей, ныне популярных под именем моделей Крипке). Он показал принципиально новые возможности интуиционистской математики, в частности, возможность формализации и позитивного использования незнания. Он дал новый подход к известному со времен Зенона Элейского14 концептуальноЗенон Элейский — греческий мудрец, живший, по традиционной хронологии, в VI веке до н. э. и прославившийся своими апориями: парадоксами пространства и времени. В частности, бесконечную делимость пространства ставит под сомнение апория Ахиллес и черепаха.
Докажем, что быстроногий Ахиллес никогда не догонит черепаху. В самом деле, пока Ахиллес добежит до того места, где была черепаха, та проползет еще немного, пока он доберется до нового ее положения, она продвинется еще дальше, Существование точек ставит под сомнение апория Стрела:
Если стрела находится в любой данный момент в одной и той же точке, то она не движется, а если она не находится в некоторый момент ни в одной точке, то где же она?
му противоречию в математической модели пространства: существуют точки и вместе с тем пространство бесконечно делимо, — он показал, что точки вводить необязательно.
16.1.5. Период после Брауэра Начиная с 1954 г. Брауэр больше не публиковал научных работ. Но целое направление уже было создано и продолжало интенсивно развиваться. В это время расцвел, в частности, советский конструктивизм, основателем которого был А. А. Марков15.
Советский конструктивизм, в отличие от интуиционизма, с самого начала взял курс на точное понятие алгоритма, которое уже сформировалось к началу 50-х годов. Первым применил точное понятие алгоритма для построения семантики интуционистских теорий американский ученый С. К. Клини в 1940–1945 гг.16 Он дал понятие реализуемости, Андрей Андреевич Марков — выдающийся русский математик. Он сын знаменитого математика А. А. Маркова, и, отталкиваясь от отца, не пожелал заканчивать математический факультет, и некоторое время работал инженером. Но затем он вернулся в математику. Работы, принесшие ему славу, были сделаны во многих областях, но в первую очередь в топологии и в алгебре, где предельно неконструктивные доказательства были скорее правилом, чем исключением. В дальнейшем он, возможно, под влиянием прикладных работ в области кодирования и декодирования (вспомним, что и Тьюринг этим занимался), перешел к конструктивной точке зрения и в некоторых отношениях стал более радикален, чем Брауэр. Это было связано и с более физическим и материалистическим мировоззрением А. А. Маркова, искавшего твердых оснований. Подходящим и надежным основанием стало точное понятие алгоритма, и А. А. Марков перестроил конструктивный взгляд таким образом, что везде были лишь алгоритмы и данные для них. В дальнейшем А. А. Марков стал пытаться обосновать саму интуиционистскую логику через теорию алгоритмов. Он столь же бескомпромиссно, как и Брауэр, отстаивал свои убеждения и столь же был терпим на практике к людям с другой точкой зрения.
Порою он заявлял следующим образом:
Необходимо помнить, что в его устах “не понимаю” означало невозможность проинтерпретировать нечто со строго конструктивной точки зрения.
С. К. Клини — выдающийся американский логик. Его фамилия читается так необычно, поскольку она сохранила остатки фризского чтения (фризы — маленький народ на островах Северного моря). Курсовой работой Клини было построение алгоритма для вычисления разности натуральных чисел (в те времена теория алгоритмов лишь начинала развиваться). Затем он дал множество красивых интерпретаций неклассических
ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА
которое может рассматриваться как подстановка конкретного понятия алгоритма в общую схему Колмогорова. Но, тем не менее, именно понятие реализуемости стало первой точной реализацией неформальной схемы, предложенной Колмогоровым. Затем (уже в 50-х гг.) Клини показал, что такую подстановку можно осуществлять разными, расходящимися между собой, способами.Н. А. Шанин17 построил алгоритм конструктивной расшифровки, аналогичный сколемизации в классической логике. Этот алгоритм выносил конструктивную задачу наружу, а проблему обоснования решения ставил таким образом, чтобы для ее доказательства можно было пользоваться классической логикой. Это еще сильнее прояснило связь классической и конструктивной логики.
Третьим направлением в широко понимаемой конструктивной математике стало то, которое ведет начало от поляков. Они предложили рассматривать лишь алгоритмические построения, но логику не менять.
Тем самым они соединили недостатки классической и конструктивной математики, хотя данной концепции и оказалось достаточно для решения нескольких задач.
Пожалуй, конец этого этапа знаменуется несколькими событиями.
Во-первых, наконец-то с помощью предложенной Д. Правитцем нормализации выводов и реализуемости по Клини было строго доказано, что во многих сильных теориях, базирующихся на интуиционистской логике, доказательство и на самом деле дает построение. Далее, были выделены важные классы формул, где классическая и конструктивная доказуемость совпадают (в частности, хорновские формулы, давшие начало теорий, написал фундаментальную книгу по математической логике [35]. Он — один из основателей теории нейронных сетей.
Н. А. Шанин — ученик А. А. Маркова. Он начинал с работы в самых абстрактных теоретико-множественных областях математики, в частности, в топологии. Именно по топологии он защитил докторскую диссертацию. Затем он всей душой воспринял конструктивную математику и начал, по примеру Брауэра, заявлять всем, что их работы никакого смысла не имеют. Ему возразили, что никакого смысла тогда не имеет и его диссертация, и он обратился в Высшую аттестационную комиссию с письмом, в котором просил лишить его степени доктора наук, поскольку его диссертация выполнена в области, не имеющей никакого смысла. Ему ответили, что по положению такая причина лишения степени не предусмотрена.
Н. А. Шанин — гораздо более крайний конструктивист, чем А. А. Марков, но и у него убежденность и научный экстремизм никогда не вырождались в личную нетерпимость по отношению к людям, придерживающимся других точек зрения (но тем, кто считались конструктивистами, порой приходилось несладко за уклонения).
языку Пролог). Были предложены несколько семантик и самой интуиционистской логики, и базирующихся на ней теорий, с помощью которых стало возможным точно исследовать вопросы о совместимости различных интуиционистских принципов и классы построений, к которым они ведут. И, наконец, Э. Бишоп (США) предложил концепцию конструктивной математики, ориентированную на соединение достоинств интуиционистского и конструктивного в советском смысле подходов. Идея была следующей: пользоваться лишь алгоритмами, но явно этого не говорить, и применять преимущества формализации намеренного незнания, показанные Брауэром. В дальнейшем мы это рассмотрим подробнее.
16.1.6. Вторая героическая эпоха:
математические результаты и попытки приложений К концу 60-х годов развитие конструктивной математики, казалось бы, выдохлось, но на самом деле выдохлась задача переформулировки результатов классической математики в конструктивной форме. И 70-е годы знаменуются всплеском результатов уже по самой интуиционистской логике и ее приложениям к математике.
Провозвестниками приложений конструктивной логики к программированию явились работы Х. Б. Карри и Р. Л. Констейбла. Карри заметил, что доказательства в импликативном фрагменте гильбертовской формулировки логики высказываний в точности соответствуют типизируемым термам в комбинаторной логике. Констейбл заметил, что, поскольку конструктивное доказательство обязательно включает построение, оно может использоваться для автоматизированного синтеза программ. Оба этих наблюдения в дальнейшем были развиты многими способами и скрещены между собой.
ИНТЕРПРЕТАЦИЯ КОЛМОГОРОВА
§ 16.2.Поскольку логические формулы понимаются в интуиционистской логике (и в других конструктивных логиках) как задачи, естественно построить интерпретацию, которая оперировала бы не с их истинностными значениями, а с решениями этих задач. Такую интерпретацию построил А. Н. Колмогоров в 1925 г. (более развитый вариант — 1932 г.). Надо заметить, что при этом Колмогоров следовал брауэровскому описанию смысла логических связок при конструктивном понимании, а его интерГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА претацию сразу же развил и уточнил ученик Брауэра А. Гейтинг. Поэтому на Западе данная интерпретация часто называется BKH-интерпретацией. Мы предпочитаем традиционный русский термин.
Как Вы помните, в теории вычислимости было установлено, что не всюду определенность (частичность) является необходимым свойством алгоритмически определяемых функций. Поэтому мы будем работать с не всюду определенными функциями и в наших интерпретациях18. Поэтому введем терминологическое различие. Оператор всюду определен для данных соответствующего типа, а функционал либо отображение — не обязательно. Если f — отображение, то !f (t) означает, что значение f (t) существует (т. е. что f (t) определено).
Определение 16.2.1. (Колмогоровская интерпретация) Пусть r A — множество решений A, и a r A означает, что a — решение A, т. е. что a r A. Пусть U — наш универс рассмотрения. Оператор, преобразующий A в r A, называется слабо колмогоровской интерпретацией, если выполнены следующие условия (пункты, помеченные, нужны лишь для логики предикатов):
1. Есть оператор join и отображения pr1, pr2, такие, что:
2. Есть операторы in1, in2 и отображение case, такие, что (!case(1, c) & case(1, c) r A) (!case(2, c) & case(2, c) r B)).
Во времена Колмогорова это еще не было ясно, и поэтому он не делал оговорки о частичности функций.
3. Есть отображение ev, такое, что * Для квантора :
4. Если нет таких a, что a r A, то 0 r ¬ A.
Если главные импликации повсюду заменить на, то интерпретация называется строго колмогоровской или просто колмогоровской.
Через ! r A обозначается тот факт, что r A непусто. Если ! r A, то A называется реализуемой в данной колмогоровской интерпретации.
Это определение отличается от оригинального в нескольких отношениях. Во-первых, у Колмогорова не было явно указанных отображений и операторов, а прямо говорилось, что множество r A & B — прямое произведение r A r B, множество r A B — прямая сумма r A r B. Пункт, соответствующий r A B, был определен только частично. Было сказано, что элементами r A B являются эффективные преобразования r A в r B, но само понятие эффективного преобразования оставалось неопределенным.
Таким образом, в сущности интерпретация Колмогорова была метаинтерпретацией, общим методом построения целого множества интерпретаций. Наше определение еще сильнее подчеркивает этот аспект и ее взаимосвязи с категорными конструкциями. Посмотрите на операторы и отображения, определявшиеся в пунктах 1 и 2. Они наводят на воспоминание об определяющих диаграммах для прямого произведения и прямой суммы (ч. I, диаграммы 5.9, 5.10).
Посмотрим, что гарантирует наше слабое определение.
Предложение 16.2.1. Выполнены следующие соотношения:
ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА
5. Не могут быть одновременно ! r A и ! r ¬ A.7. Если ! r x A(x), то ! r A(u) для некоторого u U.
8. Если ! r A(u) для некоторого u U, то ! r x A(x).
Таким образом, прямые правила вывода классической логики (за исключением правила снятия двойного отрицания, отвергнутого Брауэром) сохраняются в колмогоровской интерпретации, а реализуемость формулы вполне может служить аналогом классической истинности.
Интерпретация Колмогорова служит и сильным косвенным, полуформальным, методом анализа конструктивных утверждений. Прежде всего рассмотрим сильный закон исключенного третьего и закон двойного отрицания, критиковавшиеся Брауэром в его диссертации.
Пример 16.2.1. Реализуемость A ¬ A означает возможность либо построения реализации A, либо установления, что такой реализации не существует. А именно, для каждого A имеется элемент, из которого с помощью операции case можно получить либо реализацию A, либо реализацию ¬ A. Если этот закон принят как общий, то такая проверка должна делаться допустимыми у нас средствами. Значит, если мы интересуемся вычислимостью, то закон исключенного третьего может приниматься лишь в случае, если наш язык настолько ограничен, что все выразимые в нем свойства разрешимы.
Пример 16.2.2. Доказано, что элементарная теория действительных чисел и элементарная геометрия полны. В качестве примера приведем формулировку аксиом элементарной теории действительных чисел.
Сигнатура состоит из отношений > и =, операций сложения, умножения и вычитания и трехместного предиката, выражающего деление Div(x, y, z), истинного, когда x/y = z.
Аксиомы делятся на три группы. Первая — стандартные аксиомы поля, которые, в частности, позволяют определить константы 0 как xx и 1 как x/x для произвольного x = 0.
Вторая — аксиомы линейно упорядоченного поля.
Поскольку этот антиизоморфизм меняет местами 0 и 1, его можно считать одной из форм отрицания.
Заметим, что четырехэлементная решетка с двумя несравнимыми элементами позволяет определить два отрицания. Покажем их на чертеже.
Упражнения к § 18. 18.4.1. Чему равно (a b)?
ОСНОВЫ ЛОГИКИ ПРОТИВОДЕЙСТВИЯ
§ 18.5.Очевидно, почему Брауэр испугался собственной идеи превентивного отрицания. Он, при всей внешней революционности, как уже было показано, максимально осторожно относился к идеям математики. А данное понимание отрицания находится в грубейшем концептуальном противоречии с идеей чистой математики. Ничто не может воспрепятствовать математику сделать вывод, который следует из ранее доказанных предложений, даже если этот вывод противоречит другим ранее доказанным.
Другое дело, что такой вывод должен заставить пересмотреть некоторые из ранее принятых положений. Итак, мы видим, что грубой математической реализацией идеи Брауэра может служить правило modus tollens:
Заметим, что modus tollens точно так же согласуется с отрицанием как приведением к нежелательному результату: если из B следует нечто нежелательное, то оно следует и из A. Поэтому данное правило нельзя
ГЛАВА 18. ПРОБЛЕМА ОТРИЦАНИЯ
считать прямым и сколько-нибудь адекватным отражением идеи Брауэра. Но при сохранении хотя бы той части парадигмы современной математики, что значения и смысл математических утверждений не зависят от людей и не меняются со временем, если эти утверждения уже доказаны, дальше двинуться невозможно.Рассмотрим теперь логику меняющегося мира, в котором действуют активные субъекты. Тогда задача воспрепятствовать истинности A становится вполне осмысленной. Описание такого вида отрицания представляет нелегкую задачу. Остановимся на некоторых трудностях.
Пример 18.5.1. Рассмотрим ситуацию, где нам нужно воспрепятствовать действию, заключающемуся в повороте на 180 некоторого устройства. Тогда, если нам недопустимо прямо воздействовать на противника и есть основания полагать, что распознать состояние устройства ему будет затруднительно, лучший способ помешать противнику — самому заранее выполнить этот поворот, дабы он своим действием восстановил желаемое нам состояние.
Этот пример более или менее условный, но в восточных единоборствах известно, что часто лучший способ воспрепятствовать приему противника — помочь ему. Также и интриганы часто препятствуют чему-то нежелательному, помогая проводящему в жизнь данное действие таким образом, чтобы он якобы добился успеха, а результаты были бы прямо противоположны ожидаемым.
Итак, в логике противодействия каждое действие должно иметь обратное. Этому условию противоречит обычная совокупность функционалов колмогоровской интерпретации, поскольку, в частности, функционал, всегда принимающий одно и то же значение, необратим. Итак, в данной логике реализациями должны быть элементны некоторой группы.
Развитие логик реверсивных действий — одна из актуальных задач, которая пока еще не решалась.
ПАРАНЕПРОТИВОРЕЧИВАЯ ЛОГИКА
§ 18.6.Паранепротиворечивая логика отказывается от третьей стороны отрицания, и более того, рассматривает A и ¬ A как вполне совместимые случаи. Содержательным обоснованием этого является, например, следующее рассуждение:
Пить водку вредно для здоровья. Поэтому водку пить нельзя. Но пить водку принято в нашем обществе. Поэтому пить водку нужно.
Вариации на эту тему могут быть бесконечны.
Упражнения к § 18. 18.6.1. Какая из рассмотренных в данной главе логик является паранепротиворечивой?
Глава 19. Доказательства и программы
ИЗОМОРФИЗМ КАРРИ-ХОВАРДА
§ 19.1.Поскольку конструктивное доказательство дает умственное построение, возникает соблазн использовать его для построения и анализа программ. История такого применения доказательств, пожалуй, берет начало от забытой работы Карри [33] и от его совместной с Ховардом монографии [34], один из результатов которой мало того что изящен с математической точки зрения, но еще и выглядит необычайно соблазнительно и поэтому слишком хорошо помнится.
Рассмотрим фрагмент интуиционистской логики, в котором есть всего одна связка. Формулы данного языка изоморфны типам в типизированном -исчислении. Это — первая основа изоморфизма. Вторая основа — уже ранее неоднократно подмеченная аналогия между применением функции к аргументу и правилом modus ponens, между абстракцией и правилом дедукции. Начнем с примера.
Пример 19.1.1. Проанализируем доказательство формулы (A B) ((B C) (A C)).
Построим по этому доказательству замкнутый -терм типа ((a b) ((b c) (a c))), реализующий данную формулу. Поскольку последним применялось правило дедукции, терм должен иметь вид абстракции где мы уже знаем и тип связанной переменной, и тип подкванторного выражения. Аналогично, конкретизируя подкванторное выражение исходя из его вывода, получаем Конкретизируя последнее выражение, опять получаем -абстракцию1 :
И, наконец, рассматривая внутренний подвывод, мы видим, что в нем к x применялись f и g:
Итак, мы построили функционал, дающий композицию своих аргументов.
Переходим к точным определениям.
Пусть задано разрешимое бесконечное множество исходных типов T. Взаимно-однозначно сопоставим типы из T и пропозициональные То, что мы используем переменную x для элементарного типа, а f и g — для функциональных, является лишь стилистическим украшением.
ГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ
буквы. Тип, соответствующий импликативной формуле A, — результат замены всех пропозициональных букв на элементарные типы и Далее, каждой аксиоме теории сопоставим константу соответствующего типа. Перестроим вывод так, чтобы правило размножения применялось лишь к допущениям. Теперь терм, соответствующий выводу, строится индукцией по незавершенному выводу.Если вывод состоит лишь из аксиомы, то ей сопоставляется соответствующая константа. Если вывод состоит из допущения, то ему сопоставляется новая переменная соответствующего типа.
Если уже известны термы ta и r(ab), сопоставленные незавершенным выводам, заканчивающимся A и A B, то незавершенному выводу, заканчивающемуся применением правила сопоставляется терм (rt). Если формула получена по правилу дедукции, переменная, сопоставленная его допущению, — xa, а терм, сопоставленный его результату, — tb, то заключению правила дедукции сопоставляется x t.
Предложение 19.1.1. Существует замкнутый терм типа, соответствующего формуле A, с константами для аксиом теории Th тогда и только тогда, когда A выводима в Th.
Доказательство. Только что построенный изоморфизм обосновывает это утверждение.
Рассмотрим теперь, можно ли изоморфизм Карри-Ховарда перенести на всю логику высказываний. Препятствием к этому является отрицание. Поскольку все формулы. построенные в процессе приведения к абсурду, не могут быть выполнены в реальной ситуации, то они выпадают из построения. Итак, на самом деле программа в принципе вкладывается в доказательство, а говорить об изоморфизме означает впадать в самообман. Неудивительно, что когда изоморфизм Карри-Ховарда попытались использовать в качестве основы для доказательного программирования, это завершилось неудачами, которые, как всегда, дискредитировали все данное направление и надолго отбросили его в тень.
СИСТЕМЫ ВЫСШИХ ТИПОВ
§ 19.2.Видно, что уже изоморфизм Карри-Ховарда, несмотря на внешнюю простоту, требует интенсивного использования функционалов высших типов. Какие же операции над ними необходимы и какие достаточны, чтобы функционалы могли быть использованы в программировании?
Ответ простой. Нужны композиция и частичная параметризация функционалов, все остальное от лукавого. Именно этих двух преобразований достаточно, чтобы выразить шаги вывода. Именно эти два преобразования могут быть реализованы без потери эффективности.
Вспомним, что сложные формулы в доказательствах — это леммы, которые резко сокращают длину вывода. Поэтому значения высших типов в программировании нужны для того, чтобы сократить описания сложных процессов. Для данной цели нужно лишь, чтобы они могли моделировать выражения, получающиеся при реализации шагов логического вывода.
Итак, мы приходим к неожиданному заключению. Беда нынешних концепций работы с функционалами высших типов в системах программирования — нежелание принимать простые решения и стремление запихать в систему как можно больше возможностей, предусмотрев все невозможные запросы. Но при работе со значениями высших типов самое невинное расширение приводит к выходу за рамки логики, а практически это означает колоссальную потерю эффективности. Итак, беда здесь — отсутствие самодисциплины, теоретической культуры и полное непонимание того, что основная беда больших и сложных систем — лишние возможности.
Отметим еще одну особенность. Для классической логики мы неоднократно отмечали опасности перехода к логике высших порядков.
Эти опасности практически полностью исчезают при переходе к конструктивной логике функционалов высших типов. Поскольку способы их построения обозримы (в отличие от способов построения классических множеств), получающиеся системы оказываются полными. Но профессионалы-логики и тем более непрофессионалы-информатики по привычке избегают понятий высших типов и здесь.
ПРИЗРАКИ И КЛАССИФИКАЦИЯ ВЫВОДОВ
§ 19.3.Пожалуй, Г. С. Цейтин в 1970 г. первым заметил, что для обоснования правильности программы недостаточно тех значений, которые присутГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ ствуют в ее тексте и при ее вычислении. Нужны также величины, лишние и даже порою вредные для вычислений, но необходимые, чтобы обосновать их корректность.
Пример 19.3.1. Если мы пишем цикл типа то мы не заинтересованы (как правило) в том, чтобы он работал бесконечно. Но вычисление числа шагов цикла может быть не менее трудной задачей, чем вычисление самого цикла, и, чтобы не делать двойную работу, нужно ввести значение-призрак 2, ограничивающий сверху число шагов цикла, и доказать, что оно действительно обладает таким свойством.
Этот пример показывает еще одну сторону значений-призраков. Если мы можем построить как обычное натуральное число и достаточно быстро вычислить его (хотя бы оно и было грубой верхней оценкой числа шагов), то в цикле можно поставить аварийный завершитель, если число его повторений превзошло известную верхнюю границу. Таким образом, призраки зачастую вновь обретают плоть, если мы интересуемся диагностикой ошибок.
Рассмотрим, когда призраки появляются в выводах.
Пусть мы применили предложение о том, что некий предикат является композицией отношений, задаваемых двумя другими.
Тогда все построения, проделанные для нахождения u, нужны для обоснования, но не для программы.
Итак, практически любая нетривиальная импликация порождает призраки. Очевидные случаи, когда призраками становятся значения, построенные в отброшенных альтернативах разбора случаев либо при приведении к абсурду, добавляют еще призраков.
Имется двухпроходной алгоритм классификации выводов, который позволяет выделять значения, необходимые для построения результата вывода.
Мы специально здесь применили обозначение, вызывающее аналогии и с нестандартными числами, и с ординалами. Действительно, данный призрак не обязан быть натуральным числом, он может быть любым идеальным объектом, гарантирующим конечность реального процесса.
Схематически его можно описать следующим образом. Выходные переменные объявляются действующими. Далее идем по графу вывода вверх и объявляем действующей ту информацию в посылках выводов.
которая нужна для получения действующих частей заключения. После того, как прошли по выводу, возвращаемся вниз и пересчитываем типы, соответствующие формулам, с учетом лишь действующих их компонент.
Более того, призрачными могут быть целые типы данных. Например, оценки, используемые в доказательствах завершаемости циклов, могут принадлежать некоторому абстрактному множеству, даже более общему, чем множество ординалов, скажем, до 0, и задаваться вопросом о реализации данного множества не нужно.
ТЕОРЕМА О ВЕРИФИКАЦИИ
§ 19.4.Рассмотрим следующую задачу, которая часто ставится теоретиками и практиками для программирования.
Дана программа, доказать ее правильность.
Содержательный анализ этой задачи сразу же выявляет некоторые подозрительные места. Если уже дана программа и она работает, то зачем же доказывать ее правильность? Если же еще нет уверенности в том, всегда ли она работает, не разумнее ли было бы поставить задачу попытаться найти слабые места в данной программе? Далее, своевременно ли ставится эта задача, может быть, разумнее было бы ставить ее не тогда, когда программа уже дана, а тогда, когда она еще создается?
Словом, при получении такой задачи невольно закрадывается мысль, что в данном случае скорее нужно было бы не доказательство, а заклинание либо молитва, дабы освятить уже готовое решение.
Анализ положения дел в данной области подтверждает подозрения.
Конечно же, были случаи, когда программу доказывали, после чего в ней находили ошибку. Конечно же, теоретические системы доказательства правильности программ не работали почти ни в одном практически пригодном случае. А если где-то и работали, немедленно отказывались работать при малейших расширениях либо видоизменениях класса программ3.
Если же отходить от требований строгости, то получаемую конструкцию доказательством нельзя называть. Предложение не может быть на 80% доказанным, как и женщиГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ Но такие признаки еще не доказывают наличия принципиальных слабостей в постановке задачи, хотя и делают это вероятным. Нужно вернуться к теоретическому анализу на другом уровне.
Несмотря на все опасности слишком позитивной постановки задачи, проблема доказательства правильности программ была бы полностью оправдана, если бы удалось установить, что сложность поиска доказательства, опирающегося на уже известный текст программы, меньше, чем поиск его с самого начала, параллельно с построением программы.
Тогда бы было ясно, что игра в принципе стоит свеч.
Но, применяя установленный в предыдущих параграфах гомоморфизм доказательств в программы, можно увидеть, что это не так.
Пусть программа должна построить по входным данным, удовлетворяющим условию A(x), и выходные, удовлетворяющие условию B(x, y) 4.
Теорема 19.1. Доказательство правильности программы с увеличением длины не более чем в 3 раза перестраивается в конструктивное доказательство, из которого извлекается программа для решения той же задачи.
Заметим, что если теоретическая оценка увеличения длины вывода столь низка, то практически это чаще всего означает на самом деле его укорочение.
Итак, теоретический анализ подтверждает тот практический вывод, что восстановить обоснование уже готовой программы во всяком случае не легче, чем написать его, пока она еще развивается.
на не может быть на 80% беременна. Даже видные математики при первых попытках применения компьютера для доказательства теорем часто попадали в данную ловушку, сочтя, что громадный перебор может послужить основой, чтобы оставить некоторые случаи недоказанными. Но, как правило, быстро находились контрпримеры, выпавшие из перебора.
Мы рассматриваем случай лишь одной входной и выходной переменной, поскольку адекватной формализацией, сохраняющей гомоморфизм между доказательствами и программами, является здесь не ниже чем язык функционалов конечных типов, а в нем есть прямые произведения и прямые суммы, позволяющие свести несколько альтернативных наборов входных (выходных) данных в одну переменную.
ПРОБЛЕМА СОВМЕСТИМОСТИ ОПЕРАТОРОВ
НА ПРИМЕРЕ EXIT
§ 19.5.Известно, что с внешней стороны переход к структурному программированию выглядит как изгнание операторов перехода. Но полностью изгнать их не удается, и поэтому возникает понятие структурного перехода, который не затемняет структуру программы, а, наоборот, делает ее прозрачнее.
Общая черта таких структурных переходов состоит в том, что они идут вперед и выводят нас из программной структуры, которая сделала свое дело, но не может быть завершена по формальным мотивам.
Например, при поиске информации мы можем войти в целую последовательность операторов и процедур поиска, но, когда нужная информация найдена, все они немедленно становятся лишними и мы должны перейти в самую внешнюю процедуру, к обработке найденной информации.
Средства, предлагаемые в данном случае чистым структурным программированием, несколько неуклюжи. Предлагается завести логическую переменную, скажем, found, которая устанавливается в true при успешном поиске, и во всех разумных местах писать вместо S нечто вроде Поэтому намного естественней выглядит возможность выйти из внешней процедуры оператором типа exit(f).
Данный оператор выглядит весьма естественно, и здесь длительное время не возникало даже тени сомнения, совместим ли он со структурным программированием. Завершители стали добавляться практически везде. И лишь его логический анализ выявил, что не все так просто, и показал корни некоторых редких, но вредных ошибок в системах программирования высокого уровня.
Итак, структурный переход связан с достижением цели более высокого ранга в процессе стремления к некоторой подцели. Попытаемся формализовать его логически. В естественном выводе такую ситуацию можно описать следующим образом. Мы находились внутри вложенного вспомогательного вывода, а доказали цель объемлющего. Такая ситуация в графе вывода описывается новым структурным правилом — правилом приятной неожиданности, разрешающим завершать все вложеные друг в друга вспомогательные выводы, если во внутреннем доказана цель самого внешнего. Рассмотрим детальнее выводы с таким
ГЛАВА 19. ДОКАЗАТЕЛЬСТВА И ПРОГРАММЫ
правилом. Для простоты ограничимся пропозициональной логикой, тем более что принципиальные выводы она уже позволяет увидеть.Предложение 19.5.1. Правило приятной неожиданности допустимо в классической логике.
Доказательство. В самом деле, рассмотрим последовательность вложенных вспомогательных выводов 1,..., n, допущением самого внешнего из которых является A1, а ожидаемым результатом — B1, и так далее до самого внутреннего, допущение которого An, а цель — Bn.
Пусть во внутреннем выводе доказано A1. Тогда мы можем доказать в непосредственно объемлющем его выводе вместо получаемой из него формулы Cn1 формулу Cn1 A1. В самом деле, рассмотрим все четыре косвенных правила классической логики.
Пусть n используется в правиле приведения к абсурду. Тогда заменим это правило на правило дедукции и получим An B1. Воспользовавшись классической эквивалентностью, получаем ¬ An B1.
Правило от противного рассматривается точно так же.
Пусть теперь n используется в правиле разбора случаев. Тогда присоединяем к получившейся совокупности случаев еще один случай B1.
И, наконец, если n используется правилом дедукции, получаем An Bn B1 и по классической тавтологии — (An Bn ) B1.
Во всех промежуточных выводах вместо Ci разбором случаев получаем Ci B1.
Таким образом, протягиваем результат во внешний вспомогательный вывод.
Заметим, что процедура устранения приятной неожиданности очень напоминает описанную выше процедуру устранения стуктурного завершителя в программировании. Заметим также, что она интенсивно пользуется сугубо классическими тавтологиями.
Предложение 19.5.2. Правило приятной неожиданности превращает интуиционистскую логику в классическую.
Доказательство. Больше, чем в классическую, превратить оно не может, по предыдущему результату. Значит, достаточно вывести одну из формул, из которых следует закон исключенного третьего. Выведем форСТРУКТУРНЫЕ ЗАВЕРШИТЕЛИ мулу Пирса.
A Допущение и одновременно приятная неожиданность B Цель, которая никому уже не нужна A цель подвывода Из доказанной формулы, как известно, следует закон исключенного третьего.
Теперь проанализируем возникшие сложности. Пронос приятной неожиданности сквозь дизъюнкцию ничему не мешает. Вынос ее из импликации уже вреден. Столь же плох и вынос из доказательства приведением к абсурду, но эти части вывода никогда в программу не переходят. Итак, плохо выходить структурно из вызовов процедур, причем таких, которые являются параметрами других процедур.
Дополнительные рассмотрения с кванторами и индукцией только подтверждают этот вывод. А поскольку функционалы высших типов в программировании использовались редко и плохо, эта дополнительная ошибка оставалась укрытой. Ведь структурные выходы из разборов случаев и циклов ничему не мешают, и даже из последовательности вызовов процедур, ни одна из которых не передана в качестве параметра другой процедуре, можно также выйти безопасно.
Более того, алгоритмическими средствами установить случаи некорректности структурного завершителя невозможно, поскольку интерпретатор соответствующих теоретических конструкций пишется моментально. Разваливается структура утверждений о программе, но кого это интересует в алгоритмическом подходе, лишь бы программа исполнялась.
Литература [1] Аристотель. Первая аналитика. Сочинения, т. 1, М.: Мысль, 1975, с. 117–254.
[2] Аристотель. Вторая аналитика. Сочинения, т. 1, М.: Мысль, 1975, с. 255–346.
[3] Аристотель. Категории. Сочинения, т. 2, М.: Мысль, 1978, с. 51– [4] Аристотель. Метафизика. Сочинения, т. 1, М.: Мысль, 1975.
[5] Аристотель. Об истолковании. Сочинения, т. 1, М.: Мысль, 1975, [6] Аристотель. О софистических опровержениях. Сочинения, т. 1, М.: Мысль, 1975, с. 533–593.
[7] Аристотель. Топика. Сочинения, т. 1, М.: Мысль, 1975, с. 347–532.
[8] Дж. Булос, Р. Джеффри. Вычислимость и логика. М., Мир, 1994.
[9] Дж. Вейценбаум. Возможности вычислительных машин и человеческий разум. М.: Радио и связь, 1982.
[10] В. И. Вернадский. Труды по всеобщей истории науки. М.: Наука, [11] П. Вопенка. Математика в альтернативной теории множеств.
М.: Мир, 1983.
[12] Р. Голдблатт. Топосы. Категорный анализ логики. М.: Мир, 1983.
[13] Р. Голдблатт. Логика времени и вычислимости. М.: ОИЛКРЛ, [14] С. С. Гончаров, Ю. Л. Ершов, К. Ф. Самохвалов. Введение в логику и методологию науки. М.: Интерпракс, 1994.
[15] М. Девис. Прикладной нестандартный анализ. М.: Мир, 1980.
[16] Ю. Л. Ершов. Теория нумераций. М.: Наука, 1977.
[17] В. Г. Кановей. Аксиома выбора и аксиома детерминированности.
М.: Наука, 1984.
[18] Н. И. Конрад. У-цзы. Трактат о военном искусстве. Перевод и исследование. в кн.: Н. И. Конрад. Избранные труды. Синология.М., [19] М. Крейнович. Из чего следует закон исключенного третьего?
Тр. научных семинаров ЛОМИ, вып. 52 (1978), с. 132–145.
[20] К. Куратовский, А. Мостовский. Теория множеств. М.: Мир, [21] Л. Кэрролл. История с узелками. М.: Мир, 1973.
[22] Н. Н. Непейвода. О формализации неформализуемых понятий: автопродуктивные системы теорий. Семиотика и информатика, вып. 25 (1985), с. 46–93.
[23] Омар Хайям в кругу мудрости. Симферополь: Реноме, [24] К. М. Подниекс. Вокруг теоремы Геделя. Рига: 1981.
[25] И. Пригожин. От существующего к возникающему. М.: Наука, [26] Е. Рас ва, Р. Сикорский. Математика метаматематики. М.: Нае [27] С. П. Расторгуев, В. Н. Чибисов. Цель как криптограмма. М.:
Яхтсмен, 1996.
[28] Р. Р. Столл. Множества. Логика. Аксиоматические теории. М.:
Просвещение, 1968.
[29] В. А. Успенский. Что такое нестандартный анализ? М.: Наука,
ЛИТЕРАТУРА
[30] П. Тейяр де Шарден. Феномен человека. М.: Наука, 1987.[31] А. Т. Фоменко. Глобальная хронология. М.: МГУ, 1993.
proving. Academic Press, 1973 (русский перевод: Ч. Чень, Р. Ли.
[32] Chin-lang Cheng, R. Lee. Symbolic logic and mechanical theorem Математическая логика и автоматическое доказательство теорем.
М.: Наука, 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 (русПредметный указатель n-ка, Art, ix Currying, см. Преобразование КарCraftsmanship, ix Hypercriticism, ix Knowledge formal, viii informal, viii Mastery, viii Mathematician, viii Notion, x Science, viii Term in common language, x Адекватный, xvi
«