Линейная логика X: Изменяя мир

Linear types can change the world! 

Philip Wadler

Что может дать линейная логика программисту или проектировщику языка программирования? Слишком много, чтобы охватить всё сразу. Попытаемся рассмотреть сферы применимости, не претендуя на полноту разбора.

Вспомним, где в программировании встречаются линейные функции. Программистам знакомы понятия линейной, квадратичной, логарифмической и т.д. сложности. Речь идёт об оценке сложности алгоритмов. Линейная сложность означает, что мы можем оценить количество операций линейной функцией (от количества элементов контейнера, например).  И замечательным образом процедура, которая использует свой аргумент ровно один раз, будет обладать линейной сложностью относительно количества структурных элементов аргумента. Грубо говоря, процедура, которая принимает линейный список, сможет пройтись по элементам этого списка только один раз, что соответствует линейной сложности относительно размера списка. Это означает, что немного модифицировав правила линейной логики, можно получить языки программирования с ограничением на алгоритмическую сложность процедур. Сам Жирар предложил несколько систем типов ‒ ограниченную линейную логику (bounded linear logic, BLL), легкую линейную логику (light linear logic), элементарную линейную логику (elementary linar logic. ELL). Пока они интересны только с исследовательской точки зрения, но возможно в будущем появятся полноценные языки программирования на их основе.

Прохождение по списку в
функциональном стиле

Жирар назвал линейную логику "логикой, стоящей за логиками". Её можно представлять себе как язык более низкого уровня по сравнению с интуиционистской и классической логическими теориями. У этого языка отчетливо императивный привкус. Просто поразительно, что требование линейности, самое желанное требование для математической структуры с точки зрения исследователя, требование, которое по идее должно отдалять от реальности, приблизило логическую теорию к металлу...  Это логика в которой линейная функция естественно представляется, как процедура уничтожающая аргумент и производящая результат. Ведь если у вас есть линейное значение, то это значит, что про него более никто не знает и никто не заботится, вы можете делать с ним всё что вам заблагорассудится. Вы можете его изменить. Эта операция попросту невозможна в чисто функциональном языке, это должно звучать так же дико как изменить натуральное число. Представьте себе, что мы сегодня поменяем четыре и оно станет пятью (и дважды два станет пять). Тем не менее, если про существование данной четверки никто кроме нас не знает, мы можем её подменить пятёркой. Чем собственно и занимаются компиляторы таких языков. Они отслеживают и оптимизируют работу со значениями, которые видимы только локально. (Они могут при этом жестоко ошибиться в своих оптимизациях. Для Haskell известны программы, которые отлично работают в отладочной версии, но перестают работать при включении оптимизаций, расходуя всю наличную память. Примечательно, что одно из решений ‒ это введение примитивной операции, которая помогает сохранить линейность данных¹.)

Линейность обеспечивает очень важную вещь с точки зрения программирования ‒локальность. Если про переменную знает только одна функция, то для такой переменной не нужна сборка мусора (в том числе в виде подсчёта ссылок). Не нужны критические секции, чтоб контролировать к ней доступ в многопоточной среде ‒ ведь никто кроме нас и не будет к ней обращаться. Локальность данных делает код ясным и для программиста и для компилятора.

Кстати о параллельном программировании. Одним из применений линейной логики является описание взаимодействующих агентов. Вернее, не совсем так. Протоколы взаимодействия описываются с помощью систем сессионных типов. Но сессионные типы глубоко связаны с линейной логикой: формула линейной логики представляет собой протокол, который стороны должны соблюдать при общении, процедура избавления от лемм в доказательстве соответствует самому общению. Такое соответствие помогло построить систему типов, в которой соблюдение протокола гарантирует отсутствие взаимных блокировок. И кажется, что естественной вычислительной интерпретацией классической линейной логики являются именно такие модели. Во всяком случае в них легко интерпретировать классические дуальности линейной логики. Но этому надо будет посвятить отдельный рассказ.

Скриббл ‒ язык описания протоколов общения,
основанный на сессионных типах

Вернёмся пока к последовательному исполнению. Кроме возможности обновлять данные линейная логика может помочь с другими возможностями, присущими императивным языкам. А они нужны, ведь у чисто функционального языка есть один недостаток: никто не будет использовать такой язык для прикладного программирования. Кому нужен язык, который даже не может вывести данные в консоль? Возникает вопрос, как интегрировать в такой язык общение с внешним миром, сохранив при этом его математическую природу. Вероятно нам нужно обозначить отдельным типом функции взаимодействующие с внешним миром. Фактически считать, что они принимают на вход состояние мира и возвращают новое. И здесь идея линейности может пригодиться, поскольку  состояние внешнего мира невозможно сохранить, скопировать, но желательно не терять².

Что интересно, идея такого использования линейных типов появилась почти одновременно с линейной логикой. Вариант линейных типов ‒ уникальные типы (uniqueness types)³ используется в языке Clean, который появился в 1988 году (работа Жирара по линейной логике опубликована в 1987). Даже не знаю, имел ли представление тогда автор языка о линейной логике. 

Это лишь очень небольшая часть того, о чём можно было рассказать. Пока оставлены за скобками концепции полярности и фокусировки, связь с теорией игр, графическое представление доказательств  и многое другое. Кстати, во всей серии у нес нет ни одного примера доказательства. Поэтому прежде чем рассказывать о графических или геометрических аспектах линейной логики, посмотрим как выглядят доказательства в стандартном виде.

---

¹ Это операция явного копирования, которой в линейной системе типов можно присвоить тип dup: !A ⊸ A. Результат является независимой копией аргумента. В Haskell линейных типов нет, но смысл в том, что мы используем результат линейно.

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

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

Линейная логика IX: why so linear?

...Этот способ выйти из затруднения равносилен утверждению, что квантовомеханические уравнения движения перестают быть линейными, а точнее, становятся чрезвычайно нелинейными, когда речь заходит о существах, наделённых сознанием.  

 "Замечания относительно вопроса о соотношении сознания и тела",
 Юджин Вигнер

Для того чтобы понять, почему линейную логику назвали линейной, рассмотрим аналогию между высказываниями и аналитическими функциями. Напомню, что функция называется аналитической в окрестности какой-то точки x₀, если она представима в виде степенного ряда:

f (x) = a₀ + a₁ (x - x₀) + a₂ (x - x₀)² + ...

Если будем трактовать x в степени n как использование x n раз, то ключевое для линейной логики требование использования x ровно один раз даст нам функции, задающие прямые линии:

f (x) = с + a x

то есть линейные функции.

Вообще, слово линейный в математике имеет два разных смысла: операционный и алгебраический. Функция является линейной в операционном смысле, если использует аргумент ровно один раз (то есть так, как у нас получилось выше), линейная в алгебраическом смысле функция ‒ это функция, которая сохраняет какую-то операцию, например: 

F(A + B) = F(A) + F(B)  

Здесь F ‒ линейная по отношению к операции сложения. (Но это не обязательно должно быть сложение, сама операция может иметь разный смысл для A, B и F(A), F(B), это может быть разное сложение).  Что замечательно, при рассмотрении разных математических моделей линейной логики, в том числе той, которая привела к открытию линейной логики (в модели когерентных пространств), линейная импликация ставится в соответствие функциям линейным  уже в алгебраическом смысле.

В этой модели каждой логической формуле ставится в соответствие так называемое когерентное пространство, которое можно представлять как ненаправленный граф. Вершинами графа служат некие базовые объекты ‒ сведения, атомарные высказывания, ресурсы и т.д. Ребра обозначают совместимость, когерентность двух таких объектов. Конструкции, которые нас интересуют, представляют собой полные подграфы¹ такого графа, то есть множества объектов, которые совместимы друг с другом. Полные подграфы еще называют кликами (название произошло от клики как группы людей). Именно они считаются элементами пространства когерентности.

Логические связки конструируют новые графы на основе существующих. Так A ⊗ B будет графом пар (a, b), две пары когерентны друг другу, только если когерентны компоненты этих пар. A ⊕ B будет размеченным объединением² двух графов, в котором не появляется новых связей. Вообще, мультипликативные связки представлены парами, а аддитивные ‒объединениями. Так, A & B тоже будет размеченным объединением двух графов, в котором дополнительно любой объект из A связан с любым объектом из B. Это следует из правил де Моргана и определения линейного отрицания A^⊥. Граф A^⊥ совпадает по вершинам с графом A, но в A^⊥ два разных объекта связаны друг с другом, когда они не связаны между собой в A.

Клика как она есть

В такой модели импликация A ⇒ B задаёт набор функций на кликах. Нам, правда, подойдут не все функции, а только обладающие набором хороших свойств. К примеру, если a является подграфом b, то f (a) должна быть подграфом f (b) и тому подобные. Множеству таких функций можно сопоставить когерентное пространство. Линейная импликация A ⊸ B задаёт набор функций, для которых

f (a ∪ b) = f (a) ∪ f (b),

то есть линейных относительно операции объединения графов³. Такие функции достаточно задать на одно-элементных подграфах  ‒ это полностью определит их поведение.

Заметим, что эта операция объединения в самом формализме линейной логики отсутствует. Её можно трактовать как операцию смешивания двух однотипных ресурсов. При такой трактовке соблазнительно еще учитывать числовую меру ресурсов, их количество. В такой формальной системе можно говорить об операции дифференцирования, то есть об операции поиска линейного приближения A ⊸ B нелинейной функции A ⇒ B. Называется такая система дифференциальной линейной логикой, это направление успешно развивается с начала двухтысячных. Другим применением такого смешивания может быть логика квантовой механики, тогда под количеством ресурса мы подразумеваем вероятность события. Вообще, концепция линейности весьма близка квантовой механике, в которой квантовое состояние невозможно скопировать.

На том же перекрёстке computer science (а после обнаружения соответствия Карри-Ховарда логика неотделима от computer science) и квантовой механики находится дисциплина квантовых вычислений. Вполне логично, что языки программирования, предлагаемые для квантовых вычислений, строятся на различных вариациях линейной логики. Правда, линейная логика может пригодиться и для обычных вычислений. Об этом в следующий раз.

---

¹ То есть графы, у которых все вершины соединены ребрами.
² Объединением, в котором известно происхождение элемента, из левой ли он части или из правой.

³ При объединении мы берем все вершины двух графов, и все ребра, которыми эти вершины связаны в базовом графе. Надо учесть, что мы рассматриваем функции на кликах, а объединение двух клик не обязательно будет кликой, так что формула не всегда имеет смысл.

Линейная логика VIII: Le Canard à la Rouennaise à la Presse

...если у вас во время путешествия по Франции вдруг появится лишний денек, возьмите напрокат авто и поезжайте в город Руан. Всего полтора-два часа на северо-запад от Парижа. Это надо сделать всего ради двух вещей: снять шляпу перед великой дочерью Франции, и съесть утку по-руански в ресторане «Корона». Ни того ни другого вы больше нигде в мире сделать не сможете.

Я уже не раз говорил, что есть некоторые вещи, которые надо обязательно попробовать хоть раз в жизни. Утка по-руански в ресторане «Корона» относится к их числу. Я скажу кощунственную вещь, но я немного благодарен англосаксам, которые лишили Руан его исторической самобытности. Не случись этого, Руан непременно стал бы туристическим городом, а ресторан «Корона» — туристическим аттракционом. И вы никогда не смогли бы попробовать настоящую утку по-руански за 34 евро на две персоны.

"Номер один", Андрей Шипилов 

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

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 или B^⊥ ⊸ A. То есть, A ℘ B не позволяет получить A и B одновременно, но этот ресурс можно пустить на создание A (при наличии B^⊥) или создание B (при наличии A^⊥).
A ⊸ B — из одного ресурса A можно получить один B.
!A — возобновляемый ресурс A, доступный в неограниченном количестве, мы можем запрашивать столько сколько нам нужно (в том числе, не запрашивать совсем).
?A — возможно (но не гарантируется) наличие A, если такой ресурс имеется, мы можем использовать его столько сколько нам надо.
1 — мультипликативная истина (A ⊗ 1 эквивалентно A), ресурс, который не требует других ресурсов, чтобы его произвести.
⊥  — мультипликативная ложь (A ℘ ⊥ эквивалентно A), невозможный ресурс, нет ресурсов, которые его производят.
⊤ — аддитивная истина (A & ⊤ эквивалентно A), ⊤ поглощает любое количество ресурсов. При этом !⊤ эквивалентно 1.
0 — аддитивная ложь (A ⊕ 0 эквивалентно A), 0 производит любое количество ресурсов. ?0 эквивалентно ⊥, так что 0 тоже невозможно произвести, и получив A ⊕ 0, мы можем быть уверены, что там именно A, а не 0.

В качестве примера такой интерпретации обычно приводят ресторанное меню. Не будем использовать меню руанского ресторана «Корона», который в этом году отмечает 670 лет со дня основания. Возьмём что-нибудь попроще. Положим у нас есть такое предложение:

Суп или салат на выбор

Основное блюдо: пицца или паста

На десерт: мороженное или сорбет 

(в зависимости от наличия)

Кофе или чай (неограниченно)

Стоимость: 50 гривен

Его можно представить в виде следующей формулы:

50 грн. ⊸ (суп & салат) ⊗ (пицца & паста) ⊗ (мороженное ⊕ сорбет) ⊗ !(кофе & чай)

Можно заметить, что «или» в «суп или салат» представлено как &, поскольку выбор совершает клиент (а заведение должно иметь возможность приготовить и то и другое), но «мороженное или сорбет» использует ⊕, так как здесь выбор осуществляет заведение. Формулу можно переписать с использованием  ℘:

(50 грн.)^⊥ ℘ ((суп & салат) ⊗ (пицца & паста) ⊗ (мороженное ⊕ сорбет) ⊗ !(кофе & чай))

Таким образом, «мультипликативное или» можно трактовать как дилемму, которая задана извне. В такой ситуации мы можем потратить 50 гривен на обед или же просто заключить, что нам нужно 50 гривен, чтоб не остаться голодными, какое-либо разрешение этой дилеммы затрагивает обе части формулы (другим примером аналогичной дилеммы может служить «жизнь или кошелёк»).

В ресурсной интерпретации логики, заметно, что часть логических связок отвечает за наличие ресурсов прямо сейчас, а другая,  скорее, связана с возможностью их получения. Также заметно, что формулы линейной логики описывают взаимодействие между двумя сторонами: между клиентом и рестораном, между доказывающим и его оппонентом, между программой и её окружением. Причём одни логические связки (⊗, ⊕, !) естественно связывать с одной стороной взаимодействия, а другие (&, ℘, ?) с противоположной. Такой феномен носит называние полярности. Мы его ещё будем обсуждать подробно, но прежде мы попытаемся ответить на вопрос, который должен был возникнуть у читателя: что, собственно, линейного в линейной логике?

Линейная логика VII: Слово как действие

Среди философов слишком долго было укоренено убеждение, что «утвер­ждение» может только «описывать» положение вещей или «утверждать нечто о каком-либо факте», который при этом должен быть либо истинным, либо ложным.

«Как совершать действия при помощи слов?», Джон Лэнгшо Остин

До нашего дня удержались некоторые абсурдные музыкальные понятия прошлого, например: увертюра к опере и антрактная музыка в драматическом представлении. С чисто музыкальной точки зрения и то и другое ‒ ерунда, ибо если дело идет только о том, чтобы дать публике время занять места, то с одинаковым успехом можно до начала оперы «Фиделио» играть «Ах, мой милый Августин». Если же увертюра написана в форме попурри, то спрашивается, зачем нужно вперед заставлять публику прослушивать мотивы, которые впоследствии будут пропеты?

«Короб мыслей», Антон Рубинштейн.

Увертюра закончилась. Начинается действие. В центре этого действия находится фигура Жана Ива Жирара, человека, который своими работами предопределил развитие логики в конце 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

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^⊥) = (!A)^⊥
!(A^⊥) = (?A)^⊥

которые объясняют, каким образом нарушается симметрия, когда мы рассматриваем интуиционистское, нелинейное отрицание (! - )^⊥. Два нелинейных отрицания A дадут не A, а только ?!A. Предваряя разговор о том, как с помощью линейной логики передать конструктивные и классические теоремы, можно сказать, что интуиционистская логика не "замечает" наличие/отсутствие !, но "замечает" присутствие ?, в отличие от логики классической, которая не замечает обоих. Потому классическая логика обладает симметрией, а интуиционистская нет.

В попытке найти симметрию мы, вместо двух знакомых связок: "и" и "или", получили шесть незнакомых. Познакомится с ними ближе можно путём изучения разных моделей, благо у нас их целое меню, из этого меню мы что-нибудь выберем в следующий раз.    

---

¹ Каноническим обозначением для "мультипликативного или" является значок перевёрнутого амперсанда ⅋, но он не везде нормально отображается.

Линейная логика VI: Продолжение следует

Окончания этой потрясающей и полной драматических событий истории нельзя отыскать ни в этой, ни в другой книге, ни сейчас, ни в будущем. По правде говоря, я завёл моего героя (или героиню) в такое безвыходное и запутанное положение, что сам не знаю, как теперь с ним (или с нею) быть, а поэтому умываю руки и предоставляю ему (или ей) самостоятельно отыскать выход или оставаться в том же положении.

«Средневековый роман», Марк Твен

Механизм, который позволяет расширить аналогию между доказательствами и программами на классическую логику, называется продолжениями (continuations). Это механизм, который позволяет перейти в другую точку исполнения программы и продолжить исполнение из неё ‒ вариант нелокальной инструкции goto и аналог исключений, реализованный в некоторых языках программирования (в том числе Scheme, Standard ML и Ruby). Продолжения позволяют записать функцию, тип которой соответствует закону двойного отрицания. Но прежде чем подробно их разбирать, остановимся на том, как можно представлять отрицание в программировании.

Ранее мы использовали приём, когда отрицание A представлялось как A ⇒ ⊥, т.е. есть какой-то тип ⊥, у которого нет значений, а отрицание A ‒ это функция конструирующая значение такого типа из A. Подразумевается, что если такую функцию возможно написать, то у A значений тоже нет. При этом получается, что функцию f : A ⇒ ⊥ и вызвать то нельзя ‒ она не сможет вернуть ничего осмысленного. Возможна другая трактовка ‒ функцию можно вызвать, но она не может ничего вернуть, например, войдя в бесконечную рекурсию. То есть, тип ⊥ можно трактовать как содержащий ущербные значения, которые не дают программе завершиться. Или же, вызов f не завершается, поскольку происходит нелокальная смена контекста вычисления, прыжок в совершенно другое место программы (если язык программирования нам предоставляет такую возможность). Грубо говоря, в какой-то момент исполнения f  мы сказали: "Ой, всё" и занялись другим делом.

Что интересно, в программировании тип ⊥ обычно не встречается. Он, на самом деле, не сильно нужен, особенно если есть возможность использовать обобщенные типы. Тип ∀R R (все высказывания верны) вполне абсурден¹. Вообще, вместо специального пустого типа ⊥ можно использовать неизвестный тип R, на который  не накладывается никаких ограничений. Потом его можно заменить, в том числе на пустой тип. Такую переменную R в процессе работы с ней приходится трактовать как пустой тип, поскольку мы ничего о типе R не знаем. Другое дело, что R можно заменить и на тип содержащий значения. Так что, то что мы полагаем абсурдом, на самом деле может иметь смысл. При таком подходе закон исключённого третьего имеет следующий вид:

∀R  (A ⇒ R) + A

Закон двойного отрицания можно записать так:

∀R  ((A ⇒ R) ⇒ R) ⇒ A,

Но, неизвестный тип не может использовать одно из свойств пустого типа ‒ из него можно получить любой тип. Это условие нам понадобится, потому мы такую возможность допустим:

∀R∀S (R ⇒ S)  ⇒ (((A ⇒ R) ⇒ R) ⇒ A)

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

∀R∀S (R ⇒ S)  ⇒ ((A ⇒ R) ⇒ A) ⇒ A

Именно c него мы и начнём.  

И так, что такое продолжение. Само по себе продолжение, это функция c : ∀R  A ⇒ R, то есть обобщенная функция, которая возвращает любой указанный тип. Чтобы указать, какой тип надо вернуть, мы можем написать с : A ⇒ T или при вызове с(a) : T. Было бы странно, если бы мы по заказу могли получить любой тип, но функция с никогда не возвращает значение, она передаёт управление в другое место, вместе со своим аргументом a. Управление она передаёт в то место, где продолжение было создано. Cоздают его с помощью функции callcc (call-with-current-continuation), тип которой имеет вид:

callcc: ∀R  ((A ⇒ R) ⇒ A) ⇒ A

В callcc передаётся функция f : (A ⇒ R) ⇒ A, принимающая продолжение A ⇒ R, callcc подготавливает продолжение c и вызывает f (c: A ⇒ R). f при этом может воспользоваться c, и тогда произойдёт возврат управления в callcc, вместе с аргументом a (тогда он станет возвращаемым значением), а может и не воспользоваться, вернувшись нормальным образом (тогда, то, что вернулось из f, вернётся из callcc).² 

Таким образом, поддержка продолжений привела к тому, что классический закон Пирса получил конструктивный смысл. С помощью того же callcc можно приписать смысл и закону двойного отрицания. Единственная проблема, которая возникает, это то что callcc требует функцию f: ((A ⇒ R) ⇒ A), а в нашем распоряжении есть функции g:  (A ⇒ R) ⇒ R.  Как задать функцию f? Положить S = A, и воспользоваться функцией h: R ⇒ S, существование которой мы допустили,  тогда

f (c) = h (g (c))

Такой трюк не связан с конкретным представлением абсурдного типа ‒ если бы мы использовали ⊥ напрямую, то могли бы рассчитывать на функцию вроде absurd : ⊥ ⇒ A. Конечно, ни absurd не будет вызвана, ни исполнение g(c) не дойдёт до конца ‒ это всего лишь способ удовлетворить систему типов.

Закон исключенного третьего тоже можно побороть ‒ достаточно выписать функцию, тип которой эквивалентен его двойному отрицанию (это можно сделать), и снять двойное отрицание с помощью callcc.

Получается, что введение callcc придаёт конструктивный смысл всем истинам классической логики. Эта функция магическим образом превращает свидетельство непротиворечивости в сам объект. Это открытие, сделанное Тимоти Гриффином и описанное в статье  A formulae-as-types notion of control (1990), фактически создало новое направление в computer science, посвященное анализу конструктивного содержания классической математики.

Надо отметить, что эта конструктивность в каком-то смысле иллюзорна. Взять, к примеру, функцию g : ((A ⇒ R) ⇒ R), как она может быть устроена? Удачный вариант ‒ в её определении используется какое-то a : A, которое мы при исполнении достаём с помощью нелокального перехода (когда внутри g используется продолжение), и можем предъявить его как результат. Но есть вариант, когда внутри g используется другой нелокальный переход в неизвестное нам место. Получается теперь, что если у нас есть функция A ⇒ B, то вызвав её, мы не можем быть уверены, что в конце-концов получим B. До B мы можем в исполнении не дойти, заблудившись по дороге. 

Кроме того, важным свойством логической теории является свойство нормализуемости. Как бы мы не подставляли доказательства лемм в доказательство теоремы, мы должны всегда получать одно и тоже доказательство. С точки зрения вычисления ‒ в каком бы порядке мы не вычисляли функцию, у нас должен получаться один и тот же результат. Это свойство не выполняется для обычных языков программирования, которые позволяют общую рекурсию. Не выполняется оно и для языка, в котором есть продолжения.

Можно сказать, что конструктивный смысл у классической логики есть, но при этом каждому классическому доказательству можно приписать несколько конструкций. Это подтверждается тем, что существует несколько алгоритмов перевода классических доказательств в конструктивные, дающие разные доказательства в результате (один из них предложен Гёделем и Генценом, существуют и другие). Разные преобразования соответствуют разным способам вычисления программы, в которой используется callcc. Кстати, такие преобразования применяются и в программировании (так называемое continuation-passing-style translation) ‒ они позволяют эмулировать продолжения и аналогичные механизмы для части программы. 

Но закончим пока с логикой классической ‒ нам пора перейти к линейной логике...

---

¹ Для того чтоб задать такой тип, нужно работать в языке, который соответствует логике предикатов второго порядка ‒ логике, где предикаты могут быть функциями от высказываний (в отличие от логики первого порядка, где они могут зависеть только от базовых объектов). В программировании распространены языки, которые легко позволяют первое (зависимость типа от другого типа, т.е. обобщенные типы или шаблоны), и гораздо меньше распространены языки, которые позволяют второе (зависимость типа от конкретных значений, так называемые зависимые типы). 

² c и callcc обозначены жирным, чтобы подчеркнуть их уникальный статус. Для них невозможно написать реализацию средствами функционального языка, их необходимо трактовать как примитивные инструкции. 

Линейная логика V: Двойное отрицание

Лекция на филфаке. Старый профессор говорит:

— В русском языке двойное отрицание может означать утверждение. Но ни в одном языке мира двойное утверждение не может означать отрицание.

Раздается голос с задней парты:
— Ну да, конечно…

Старый анекдот

Однажды во время лекции оксфордский философ Джон Ленгшо Остин высказал мысль, что хотя двойное отрицание в английском языке означает утверждение, нет такого языка, в котором двойное утверждение означало бы отрицание. На что Сидни Моргенбессер, в то время студент, ответил с пренебрежением в голосе: "Да, да...".

Английский вариант анекдота как случай, произошедший с философом Сидни Моргенбессером

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

¬¬A ⇏ A

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

A ⇒ ¬¬A

Это достаточно легко показать, если вспомнить, что конструктивное отрицание представляет собой функцию, а ¬¬A означает (A ⇒ ⊥) ⇒ ⊥, то есть "дайте мне функцию из A в абсурдный тип, и я получу абсурд". Если при этом есть свидетельство a : A, то такую функцию написать легко:

f : (A ⇒ ⊥) ⇒ ⊥

f ( g : A ⇒ ⊥) =  g ( a ) 

То есть, функция f принимает в качестве параметра функцию g :  A ⇒ ⊥ и, имея свидетельство a,  передаёт его в g, приходя к абсурду. Не так уж важно сейчас, что функция f не может быть вызвана, важно то, что мы можем её задать. Согласно соответствию Карри‒Ховарда это означает доказуемость нашего утверждения. Кроме того, доказуемо

 ¬¬¬A ⇒ ¬A 

Доказательство достаточно просто следует из предыдущего утверждения. Положим у нас есть функция h, которая из ¬¬A конструирует ⊥ (это, напоминаю, и есть свидетельство  ¬¬¬A). Как из этого получить функцию, которая из A конструирует ⊥? Достаточно из A сконструировать ¬¬A и передать его в h. 

То есть, для некоторых конструктивных утверждений выполняются классические законы. Для логики высказываний справедлива теорема, что если в классической логике доказуемо A, то в интуиционистской логике доказуемо ¬¬A. Она носит название теорема Гливенко. 

Когда рассматривается логика предикатов, то теорема Гливенко неверна. Тем не менее, существует способ преобразовать классическую теорему в конструктивную. Один из методов преобразования придуман Гёделем и Генценом. Грубо говоря, он заключается в том, чтоб подобавлять отрицания в разные места высказывания (под кванторы, в том числе). 

Получается, что неконструктивные доказательства  классической математики не являются неверными с точки зрения математики конструктивной, они просто доказывают другие утверждения. Если конструктивная теорема существования должна презентовать в качестве свидетельства искомый объект, то классической достаточно предъявить свидетельство непротиворечивости. В конструктивной математике такими свидетельствами можно оперировать почти также как обычными объектами (они, можно сказать, задают модальность "не исключено, что ..."). Классическая же математика одно от другого просто не отличает. Таким образом, конструктивная логика не обладает меньшей доказательной силой, но различает больше утверждений. 

Означает ли это, что классическая математика может считаться частным случаем конструктивной? Увы, на сегодняшний момент не может. В классической математике используются существенно неконструктивные приёмы. За них отвечает так называемая аксиома выбора. Например, такое обыденное утверждение как «действительные числа можно упорядочить», доказываемое с помощью аксиомы выбора, есть пример утверждения, которому пока не удалось приписать конструктивный смысл. 

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

Линейная логика IV: Доказательства и программы

Эти записи посвящены старой аналогии между доказыванием теорем и программированием: доказательство похоже на программу, программа похожа на доказательство. Возможно, причиной того, что эта аналогия, известная как доказательства-как-программы, утверждения-как-типы или соответствие Карри–Ховарда, всё еще кажется новой, хотя ей уже несколько десятилетий, кроется в том, что она вдохновляет и математиков и программистов. Программист может сказать себе: "Я не только трачу время, программируя целый день – я доказываю теоремы". Математик в свою очередь может сказать себе: "Я не только трачу время, доказывая теоремы целый день – я программирую".

«Logical basis of evaluation order and pattern matching», Ноам Зайлбергер