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

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

18.3. ЛОГИКА С СИЛЬНЫМ ОТРИЦАНИЕМ

471

одно из определенных состояний

). Совместной индукцией определя-

ются понятия истинности и ложности формулы.

p |= A и p |= B

p |= A & B

p =| A или p =| B

p =| A & B

p |= A

или p |= B

p |= A ∨ B

p =| A и p =| B

p =| A ∨ B

p |=

p =| ∼ A

p =| A

p |=∼ A

Если q |= A, то q |= B

для всех p 4 q

p |= A ⇒ B

p |= A

и p =| B

p =| A ⇒ B

Есть такое c ∈ U

что p |= A(c)

p |= ∃x A(x)

Для всех p 4 q и для всех

c ∈ U

q =| A(c)

p =| ∃x A(x)

Для всех p 4 q и для всех

c ∈ U

q |= A(c)

p |= ∀x A(x)

Есть такое c ∈ U

что p =| A(c)

p =| ∀x A(x)

(18.10)

Заметим, что обычное интуиционистское отрицание выражается через

сильное отрицание и импликацию. А именно,

A ⇔ (A ⇒∼ A)

(18.11)

Теперь легко построить модель, в которой ложен сильный закон исклю-

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

известно

A. Тогда

и одновременно

∼ A

Сильное отрицание может пониматься как конструктивное опровер-

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

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

для сильного отрицания (построение которой оставлено Вам в качестве

упражнения) может быть интерпретирована как построение програм-

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

осмысленного сообщения об ошибке в случае неудачи

Но никто не гарантирует, что неизвестное высказывание когда-нибудь будет уточне-

но.

Все, кто имели дело с программами, прекрасно понимают разницу между информа-

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

граммы.

472

ГЛАВА 18. ПРОБЛЕМА ОТРИЦАНИЯ

Упражнения к § 18.3

18.3.1. Дайте определение реализуемости для формул логики с силь-

ным отрицанием.

18.3.2. Как видоизменится доказательство теоремы полноты для логики

с сильным отрицанием?

18.3.3. Рассмотрим следующее рассуждение.

∼∼ A для любой форму-

лы A означает то же самое, что и A. Рассмотрим теперь A ⇒ B.

Оно эквивалентно ∼∼ (A ⇒ B), но ∼ (A ⇒ B) эквивалентно

A &∼ B. Таким образом, A ⇒ B эквивалентно ∼ (A &∼ B). Но,

по правилам формулировки отрицания, последняя формула экви-

валентна ∼ A ∨∼∼ B, что эквивалентно ∼ A ∨ B. Таким обра-

зом, A ⇒ B эквивалентно ∼ A ∨ B. Взяв частный случай A ⇒ A,

получаем ∼ A ∨ A, а данная формула не то что невыводима, а да-

же может быть ложной в модели Крипке. В чем дело?

18.3.4. Можно ли рассматривать сильное отрицание в классической ло-

гике?

§ 18.4. ЛОГИКА НЕПОЛНОЙ ИНФОРМАЦИИ

Одна из проблем, на которую мы уже неоднократно наталкивались, —

неполные структуры, частично-определенные операции и прочее по-

добное. Эта проблема оказывается связана с вариациями понятия от-

рицания.

В самом деле, рассмотрим простейшую логику неполной информа-

ции, созданную С. К. Клини. В ней три логических значения — истина,

ложь и бессмыслица (неопределенность)

u. Значение формулы, содер-

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

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

Так, например, ⊥ & u — ложь, а значение u ⇒ u само есть u.

При такой интерпретации

u = u

Алгебраической интерпретацией подобных структур являются ре-

шетки с инволюцией.

Определение 18.4.1.

Решетка

называется

решеткой с инволюцией

,если

задан ее антиизоморфизм

∼

на себя как упорядоченного множества, та-

кой, что

∀a ∼∼ a = a

18.5. ОСНОВЫ ЛОГИКИ ПРОТИВОДЕЙСТВИЯ

473

Напомним, что отображение называется антиизоморфизмом чумов,

если оно взаимно однозначно и x < y ⇔ f(x) > f(y).

Поскольку этот антиизоморфизм меняет местами

0 и 1, его можно

считать одной из форм отрицания.

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

элементами позволяет определить два отрицания. Покажем их на чер-

теже.

a =

b =∼ a b =

a =∼ b

(18.12)

Упражнения к § 18.4

18.4.1. Чему равно

∼ (a ∩ b)?

§ 18.5. ОСНОВЫ ЛОГИКИ ПРОТИВОДЕЙСТВИЯ

Очевидно, почему Брауэр испугался собственной идеи превентивного

отрицания.Он,при всей внешней революционности,как уже было пока-

зано, максимально осторожно относился к идеям математики. А данное

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

воречии с идеей чистой математики. Ничто не может воспрепятствовать

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

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

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

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

ческой реализацией идеи Брауэра может служить правило modus tollens:

A ⇒ B

(18.13)

Заметим, что modus tollens точно так же согласуется с отрицанием как

приведением к нежелательному результату: если из

B следует нечто не-

желательное, то оно следует и из A. Поэтому данное правило нельзя

474

ГЛАВА 18. ПРОБЛЕМА ОТРИЦАНИЯ

считать прямым и сколько-нибудь адекватным отражением идеи Брауэ-

ра. Но при сохранении хотя бы той части парадигмы современной мате-

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

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

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

Рассмотрим теперь логику меняющегося мира, в котором действуют

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

A ста-

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

ставляет нелегкую задачу. Остановимся на некоторых трудностях.

Пример 18.5.1.

Рассмотрим ситуацию, где нам нужно воспрепятство-

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

180

◦

некоторого устрой-

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

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

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

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

желаемое нам состояние.

Этот пример более или менее условный, но в восточных единобор-

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

тивника — помочь ему. Также и интриганы часто препятствуют чему-то

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

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

противоположны ожидаемым.

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

ратное. Этому условию противоречит обычная совокупность функци-

оналов колмогоровской интерпретации, поскольку, в частности, функ-

ционал, всегда принимающий одно и то же значение, необратим. Итак,

в данной логике реализациями должны быть элементны некоторой груп-

пы.

Развитие логик реверсивных действий — одна из актуальных задач,

которая пока еще не решалась.

§ 18.6. ПАРАНЕПРОТИВОРЕЧИВАЯ ЛОГИКА

Паранепротиворечивая логика отказывается от третьей стороны отри-

цания, и более того, рассматривает A и

как вполне совместимые

18.6. ПАРАНЕПРОТИВОРЕЧИВАЯ ЛОГИКА

475

случаи. Содержательным обоснованием этого является, например, сле-

дующее рассуждение:

Пить водку вредно для здоровья. Поэтому водку

пить нельзя. Но пить водку принято в нашем об-

ществе. Поэтому пить водку нужно.

(18.14)

Вариации на эту тему могут быть бесконечны.

Упражнения к § 18.6

18.6.1. Какая из рассмотренных в данной главе логик является паране-

противоречивой?

Глава 19. Доказательства

и программы

§ 19.1. ИЗОМОРФИЗМ КАРРИ-ХОВАРДА

Мартышкам стало холодно зимой,

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

«Согреемся теперь, конец мученьям»—

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

(Рудаки. [23, стр. 212])

Поскольку конструктивное доказательство дает умственное постро-

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

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

ло от забытой работы Карри [33] и от его совместной с Ховардом моно-

графии [34],один из результатов которой мало того что изящен с матема-

тической точки зрения, но еще и выглядит необычайно соблазнительно

и поэтому слишком хорошо помнится.

Рассмотрим фрагмент интуиционистской логики, в котором есть все-

го одна связка ⇒. Формулы данного языка изоморфны типам в типи-

зированном λ-исчислении. Это — первая основа изоморфизма. Вторая

основа — уже ранее неоднократно подмеченная аналогия между при-

менением функции к аргументу и правилом

modus ponens

, между λ-

абстракцией и правилом дедукции. Начнем с примера.

19.1. ИЗОМОРФИЗМ КАРРИ-ХОВАРДА

477

Пример 19.1.1.

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

(A ⇒ B) ⇒

((B ⇒ C) ⇒ (A ⇒ C))

∗ A ⇒ B



∗ B ⇒ C



∗ A



A ⇒ C

(B ⇒ C) ⇒ (A ⇒ C)

(A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C))

(19.1)

Построим по этому доказательству замкнутый

-терм типа

((a → b) →

((b → c) → (a → c)))

, реализующий данную формулу. Поскольку

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

абстракции

λf

(a→b)

. (∙∙∙)

((b→c)→(a→c))

, (19.2)

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

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

ходя из его вывода, получаем

λf

(a→b)

. λg

(b→c)

. (∙∙∙)

(a→c)

. (19.3)

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

-абстракцию

λf

(a→b)

. λg

(b→c)

. λx

. (∙∙∙)

. (19.4)

И, наконец, рассматривая внутренний подвывод, мы видим, что в нем к

применялись

λf

(a→b)

. λg

(b→c)

. λx

. (g(fa)). (19.5)

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

тов.

Переходим к точным определениям.

Пусть задано разрешимое бесконечное множество исходных типов

T . Взаимно-однозначно сопоставим типы из T и пропозициональные

То, что мы используем переменную x для элементарного типа, а f и g — для функ-

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

478

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

буквы. Тип, соответствующий импликативной формуле A, — резуль-

тат замены всех пропозициональных букв на элементарные типы и ⇒

на →.

Далее, каждой аксиоме теории сопоставим константу соответству-

ющего типа. Перестроим вывод так, чтобы правило размножения при-

менялось лишь к допущениям. Теперь терм, соответствующий выводу,

строится индукцией по незавершенному выводу.

Если вывод состоит лишь из аксиомы, то ей сопоставляется соот-

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

поставляется новая переменная соответствующего типа.

Если уже известны термы

и r

(a→b)

, сопоставленные незавершен-

ным выводам, заканчивающимся A и A ⇒ B, то незавершенному вы-

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

A A ⇒ B

сопоставляется терм (rt). Если формула получена по правилу дедук-

ции, переменная, сопоставленная его допущению, — x

, а терм, сопо-

ставленный его результату, — t

, то заключению правила дедукции со-

поставляется λx t.

Предложение 19.1.1. Существует замкнутый терм типа, соответ-

ствующего формуле

A, с константами для аксиом теории Th тогда

и только тогда, когда A выводима в Th.

Доказательство. Только что построенный изоморфизм обосновывает

это утверждение

Рассмотрим теперь, можно ли изоморфизм Карри-Ховарда перене-

сти на всю логику высказываний. Препятствием к этому является отри-

цание. Поскольку все формулы. построенные в процессе приведения к

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

ют из построения. Итак, на самом деле программа в принципе вклады-

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

в самообман. Неудивительно, что когда изоморфизм Карри-Ховарда по-

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

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

тировали все данное направление и надолго отбросили его в тень.

19.2. СИСТЕМЫ ВЫСШИХ ТИПОВ

479

§ 19.2. СИСТЕМЫ ВЫСШИХ ТИПОВ

Видно,что уже изоморфизм Карри-Ховарда,несмотря на внешнюю про-

стоту, требует интенсивного использования функционалов высших ти-

пов. Какие же операции над ними необходимы и какие достаточны, что-

бы функционалы могли быть использованы в программировании?

Ответ простой. Нужны композиция и частичная параметризация

функционалов, все остальное от лукавого. Именно этих двух преобра-

зований достаточно, чтобы выразить шаги вывода. Именно эти два пре-

образования могут быть реализованы без потери эффективности.

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

которые резко сокращают длину вывода. Поэтому значения высших ти-

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

сложных процессов. Для данной цели нужно лишь, чтобы они могли

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

ческого вывода.

Итак, мы приходим к неожиданному заключению. Беда нынешних

концепций работы с функционалами высших типов в системах програм-

мирования — нежелание принимать простые решения и стремление за-

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

невозможные запросы. Но при работе со значениями высших типов са-

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

тически это означает колоссальную потерю эффективности. Итак, беда

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

ное непонимание того,что основная беда больших и сложных систем —

лишние возможности.

Отметим еще одну особенность. Для классической логики мы не-

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

Эти опасности практически полностью исчезают при переходе к кон-

структивной логике функционалов высших типов. Поскольку способы

их построения обозримы (в отличие от способов построения класси-

ческих множеств), получающиеся системы оказываются полными. Но

профессионалы-логики и тем более непрофессионалы-информатики по

привычке избегают понятий высших типов и здесь.

§ 19.3. ПРИЗРАКИ И КЛАССИФИКАЦИЯ ВЫВОДОВ

Пожалуй, Г. С. Цейтин в 1970 г. первым заметил, что для обоснования

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

480

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

ствуют в ее тексте и при ее вычислении. Нужны также величины, лиш-

ние и даже порою вредные для вычислений, но необходимые, чтобы

обосновать их корректность.

Пример 19.3.1.

Если мы пишем цикл типа

while

S; (19.6)

то мы не заинтересованы (как правило) в том, чтобы он работал беско-

нечно. Но вычисление числа шагов цикла может быть не менее трудной

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

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

, ограничивающий сверху чи-

сло шагов цикла, и

доказать

, что оно действительно обладает таким

свойством.

Этот пример показывает еще одну сторону значений-призраков.Если

мы можем построить

как обычное натуральное число и достаточно

быстро вычислить его (хотя бы оно и было грубой верхней оценкой чи-

сла шагов), то в цикле можно поставить аварийный завершитель, если

число его повторений превзошло известную верхнюю границу

. Таким

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

емся диагностикой ошибок.

Рассмотрим, когда призраки появляются в выводах.

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

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

A(t, u) A(u, r) ∀x, y, z(A(x, y) & B(y, z) ⇒ C(x, z))

C(t, r)

Тогда все построения, проделанные для нахождения u, нужны для обо-

снования, но не для программы.

Итак, практически любая нетривиальная импликация порождает

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

построенные в отброшенных альтернативах разбора случаев либо при

приведении к абсурду, добавляют еще призраков.

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

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

вывода.

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

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

натуральным числом, он может быть любым идеальным объектом, гарантирующим ко-

нечность реального процесса.