Среди философов слишком долго было укоренено убеждение, что «утверждение» может только «описывать» положение вещей или «утверждать нечто о каком-либо факте», который при этом должен быть либо истинным, либо ложным.
«Как совершать действия при помощи слов?», Джон Лэнгшо Остин
До нашего дня удержались некоторые абсурдные музыкальные понятия прошлого, например: увертюра к опере и антрактная музыка в драматическом представлении. С чисто музыкальной точки зрения и то и другое ‒ ерунда, ибо если дело идет только о том, чтобы дать публике время занять места, то с одинаковым успехом можно до начала оперы «Фиделио» играть «Ах, мой милый Августин». Если же увертюра написана в форме попурри, то спрашивается, зачем нужно вперед заставлять публику прослушивать мотивы, которые впоследствии будут пропеты?
«Короб мыслей», Антон Рубинштейн.
Увертюра закончилась. Начинается действие. В центре этого действия находится фигура Жана Ива Жирара, человека, который своими работами предопределил развитие логики в конце XX века, и который переопределил саму логику в XXI, но речь сейчас о более раннем времени. В начале 80-ых Жирар занимался изучением моделей интуиционистской логики. В одной из них он обнаружил, что логические операции там можно разложить на более примитивные ‒ это и подвигло его на разработку линейной логики. Система получилась интересной, но необычной, уж больно странными были требования налагаемые на утверждения. Правда, не обязательно трактовать объекты, с которыми работает линейная логика, как утверждения, возможны и другие трактовки, например, как планы и действия, ресурсы и их преобразования, диалоги и сюжеты, игры и стратегии, химические реакции и программы с параллельным вычислением.
Мы пока сосредоточимся на логической трактовке. Ограничение состоит в следующем: в стандартном случае в линейной логике каждую гипотезу полагается использовать ровно один раз. То есть, мы обязаны использовать гипотезу, и не можем использовать более одного раза. В логике такое ограничение позволяет ввести вариант закона двойного отрицания и правил де Моргана, восстановив симметрию классической логики внутри конструктивной теории. Это достигается за счёт увеличения количества логических связок ‒ теперь у нас два "и" и два "или". Рассмотрим их:
A ⊗ B — "мультипликативное и", A и B справедливы одновременно, их вывод использует разные наборы гипотез.
A ⊕ B — "аддитивное или", справедливо А или справедливо B, в каждом конкретном случае известно, что именно. Такую операцию можно трактовать как операцию внешнего выбора. Мы не можем выбрать, что произошло, но можем узнать.
A & B — "аддитивное и", можно вывести и A и B, но надо выбрать только одно из них, у них общий набор гипотез. Это операция внутреннего выбора.
A ℘ B — "мультипликативное или",¹ связка, которая указывает на зависимость между утверждениями ‒ возможно, что справедливо A или B, но неизвестно, что именно. Узнать, что выполняется можно лишь при наличии дополнительной информации (например, что не выполняется A, тогда можно вывести B и наоборот).
В линейной логике даже понятия истины и лжи присутствуют в двух вариантах: 0 и ⊤ ‒ аддитивная ложь и истина, ⊥, 1 ‒ мультипликативная ложь и истина. По одной константе на каждую из связок.
Чтоб говорить о двойном отрицании, сначала нужно ввести само понятие отрицания. В классической презентации линейной логики отрицание не является связкой, скорее это отношение дуальности между утверждениями. Вводится оно так. Для любого утверждения p можно сформулировать дуальное утверждение p⊥. Для простых, неразложимых на части утверждений, мы требуем чтобы
p⊥⊥ = p
Для сложных высказываний дуальное утверждение вводится с помощью следующих тождеств:
(A ⊗ B)⊥ = A⊥℘ B⊥
(A & B)⊥ = A⊥⊕ B⊥
(A ⊕ B)⊥ = A⊥& B⊥
(A ℘ B)⊥ = A⊥⊗ B⊥
(A & B)⊥ = A⊥⊕ B⊥
(A ⊕ B)⊥ = A⊥& B⊥
(A ℘ B)⊥ = A⊥⊗ B⊥
Чтоб читатель не вглядывался в обилие разных странных значков, правила достаточно просты: при отрицании свойство аддитивности/мультипликативности сохраняется (а округлость значка - нет). Правила сформулированы так, чтоб для любого утверждения A
A⊥⊥ = A
То есть, мы ввели закон исключенного третьего и правила де Моргана аксиоматически. При этом, линейная логика в любом из своих вариантов является конструктивной теорией. Как построить язык программирования, в котором эти правила выполняются хотя бы как эквивалентности, есть отдельная тема.
Какие еще операции есть в линейной логике? Мы не ввели линейную операцию следования, и в классической линейной логике она не является базовой. Но если обратить внимание на "мультипликативное или", то в нём угадывается алгоритмическое содержание, это почти функция. Это не случайно, линейную импликацию определяют как
A ⊸ B = A⊥℘ B
A⊥℘ B можно прочесть как "мне не хватает одного A, чтоб построить одно B" (или если я отдам вам одно B, мне будет не хватать одного A). То есть, линейную импликацию можно представить как действие, которое можно совершить над A, превратив его в B. A в процессе перестаёт существовать. Подставив вместо B ⊥ мы получим знакомое
A ⊸ ⊥ = A⊥℘ ⊥, что равносильно A⊥
Таким образом, линейное отрицание является более сильным, чем интуиционистское отрицание ‒ чтобы утверждать A⊥ необходимо прийти к противоречию, имея одну гипотезу A без возможности её дублировать.
Чтобы линейная логика могла доказывать обычные теоремы, нам необходимо ввести дополнительные одноместные логические связки ‒ ! и ?:
! — задаёт модальность "конечно", гипотезы такого типа можно невозбранно дублировать и удалять, если среди гипотез еще остаётся копия.
? — задаёт дуальную модальность "не исключено". Очень классическая модальность. С точки зрения линейной логики свидетельство непротиворечивости, которое является конструктивным содержанием классических теорем, можно трактовать как "конечно не исключено, что ...".
Чтобы линейная логика могла доказывать обычные теоремы, нам необходимо ввести дополнительные одноместные логические связки ‒ ! и ?:
! — задаёт модальность "конечно", гипотезы такого типа можно невозбранно дублировать и удалять, если среди гипотез еще остаётся копия.
? — задаёт дуальную модальность "не исключено". Очень классическая модальность. С точки зрения линейной логики свидетельство непротиворечивости, которое является конструктивным содержанием классических теорем, можно трактовать как "конечно не исключено, что ...".
Связки ! и ? называют экспоненциальными поскольку ! переводит "аддитивное и" в мультипликативное (? аналогичным образом поступает с или), подобно тому как экспонента переводит сумму в произведение:
!(A & B) = !A ⊗ !B
?(A ⊕ B) = ?A ℘ ?B
?(A ⊕ B) = ?A ℘ ?B
Экспоненциальные связки связаны соотношениями:
?(A⊥) = (!A)⊥
!(A⊥) = (?A)⊥
которые объясняют, каким образом нарушается симметрия, когда мы рассматриваем интуиционистское, нелинейное отрицание (! - )⊥. Два нелинейных отрицания A дадут не A, а только ?!A. Предваряя разговор о том, как с помощью линейной логики передать конструктивные и классические теоремы, можно сказать, что интуиционистская логика не "замечает" наличие/отсутствие !, но "замечает" присутствие ?, в отличие от логики классической, которая не замечает обоих. Потому классическая логика обладает симметрией, а интуиционистская нет.!(A⊥) = (?A)⊥
В попытке найти симметрию мы, вместо двух знакомых связок: "и" и "или", получили шесть незнакомых. Познакомится с ними ближе можно путём изучения разных моделей, благо у нас их целое меню, из этого меню мы что-нибудь выберем в следующий раз.
¹ Каноническим обозначением для "мультипликативного или" является значок перевёрнутого амперсанда ⅋, но он не везде нормально отображается.
Комментариев нет:
Отправить комментарий