Линейная логика 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. Она носит название теорема Гливенко. 

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

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

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

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

Линейная Логика II: предыстория. Классическая логика

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

Готфрид Вильгельм Лейбниц

Если рассказывать предысторию линейной логики, то с какого периода начать? С Аристотеля? Или, быть может, с Лейбница? Или начать с Джона Буля и Готлоба Фреге? Бертрана Рассела и Альфреда Уайтхеда? Или с критики Брауэром программы Давида Гильберта? 

Прежде чем излагать критику, следует рассмотреть критикуемый объект. Не вдаваясь в подробности, можно сказать, что к началу XX века в математике существовало целое логицистское направление, основная идея которого заключалась в полной формализации математики, и сведении, таким образом, математики к логике. К какой же именно логике надо свести математику? Такой вопрос, разумеется, тогда не ставился, ибо на тот момент мыслилась только одна логика. Тем не менее, рассмотрим классический вариант математической логики подробно.

Логика оперирует высказываниями. Есть набор базовых, содержанием которых логика не интересуется. Важно лишь то, что каждое из них истинно либо ложно. Из них с помощью логических связок можно строить сложные высказывания. Логические связки бывают следующие:

• "и": A ⋀ B — если верно A ⋀ B, то верны и A и B, и наоборот.
• "или": A ⋁ B — если верно A ⋁ B, то верно по крайней мере одно из высказываний A или B, и наоборот.
• "не":  ¬A — выполняется в том случае, когда A неверно.
• "следует": A → B — его можно определить как ¬A ⋁ B. В формальной логике считается, что из правды можно вывести любую правду, а из лжи — всё что угодно. Что оправдывает такое определение. Если выполняется A → B и B → A, то можно писать A ↔ B.

Этих связок хватает, чтобы строить самую простую логику — логику высказываний. Более сложной и интересной вещью является логика предикатов. Предикат — это логическая функция, высказывание о нефиксированном объекте.¹ Его можно понимать как недостроенное высказывание — если предоставить объект, оно превращается в обычное. (природу самого объекта мы пока вынесем за скобки). Другим способом превращения предиката в высказывание является применение кванторов всеобщности и существования:

• ∀x P(x) — для всех x выполняется свойство P
• ∃x P(x) — существует x для которого выполняется свойство P

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

∀x P(x) ≡ P(a) ⋀ P(b) ⋀ P(c) ⋀ ... 

∃x P(x) ≡ P(a) ⋁ P(b) ⋁ P(c) ⋁ ...

для всех значений, которые можно подставить вместо x. Математиков, строивших первые формализмы, смущала необходимость вместе с квантором вводить и переменную, которую к тому же надо отличать от тех переменных, что уже используются внутри P. Было показано, что можно построить логику без переменных — комбинаторную логику.

Что нам еще нужно, чтобы пользоваться классической логикой? Мы знаем как строить высказывания, но не знаем как строить доказательства этих высказываний. То есть, нам нужны правила, по которым из одних высказываний, можно получить другие высказывания — правила вывода. Кроме того, нам нужны аксиомы — правила построения верных высказываний.² Если мы указали аксиому, частный случай которой представляет наше высказывание, то мы его доказали, при том чисто синтаксически. Если мы пользуясь правилами вывода прошли от аксиом к нашему высказыванию, то мы его доказали, построив дерево вывода.

Весь список кораблей аксиом и правил вывода приводить не имеет большого смысла. Они естественным образом определяются знакомыми всем свойствами логических связок (от A ⋀ B можно перейти к A, от A можно перейти к A ⋁ B, и т.д.). Самым важным правилом вывода, наверное, следует считать modus ponens: из двух высказываний A и A → B можно вывести B. Вообще, линия между правилами вывода и аксиомами размыта — одно и то же свойство логической связки может быть в разных формализациях передано как аксиомой, так и правилом вывода, в принципе, при соответствующей формулировке аксиом из всех правил вывода можно оставить только modus ponens. Если же используются несколько правил вывода, то соответствующие аксиомы становятся теоремами.

Что для нас существенно, что среди аксиом классической логики есть закон исключенного третьего A ⋁ ¬A. Или равносильный ему закон двойного отрицания ¬¬A  → A. Они делают возможным построение доказательств от противного. Они также есть причиной замечательных тождеств де Моргана:

¬ ( A ⋁ B ) ↔ ¬A ⋀ ¬B

¬ ( A ⋀ B ) ↔ ¬A ⋁ ¬B

делающих классическую логику столь симметричной. Схожей природы правило отрицания для кванторов:

¬ ∃x P(x) ↔ ∀x ¬ P(x)

¬ ∀x P(x) ↔ ∃x ¬ P(x)

И именно закон исключенного третьего и правило отрицания были подвергнуты критике со стороны основателя интуиционистского направления Брауэра. Но об этом в следующий раз.

---

¹ Предикат конечно может зависеть от нескольких переменных, так что изложение здесь нестрогое
² Строго говоря, аксиома — это конкретное высказывание, полагаемое верным, правила построения верных высказываний называются схемами аксиом