Окончания этой потрясающей и полной драматических событий истории нельзя отыскать ни в этой, ни в другой книге, ни сейчас, ни в будущем. По правде говоря, я завёл моего героя (или героиню) в такое безвыходное и запутанное положение, что сам не знаю, как теперь с ним (или с нею) быть, а поэтому умываю руки и предоставляю ему (или ей) самостоятельно отыскать выход или оставаться в том же положении.
«Средневековый роман», Марк Твен
Механизм, который позволяет расширить аналогию между доказательствами и программами на классическую логику, называется продолжениями (continuations). Это механизм, который позволяет перейти в другую точку исполнения программы и продолжить исполнение из неё ‒ вариант нелокальной инструкции goto и аналог исключений, реализованный в некоторых языках программирования (в том числе Scheme, Standard ML и Ruby). Продолжения позволяют записать функцию, тип которой соответствует закону двойного отрицания. Но прежде чем подробно их разбирать, остановимся на том, как можно представлять отрицание в программировании.
Ранее мы использовали приём, когда отрицание A представлялось как A ⇒ ⊥, т.е. есть какой-то тип ⊥, у которого нет значений, а отрицание A ‒ это функция конструирующая значение такого типа из A. Подразумевается, что если такую функцию возможно написать, то у A значений тоже нет. При этом получается, что функцию f : A ⇒ ⊥ и вызвать то нельзя ‒ она не сможет вернуть ничего осмысленного. Возможна другая трактовка ‒ функцию можно вызвать, но она не может ничего вернуть, например, войдя в бесконечную рекурсию. То есть, тип ⊥ можно трактовать как содержащий ущербные значения, которые не дают программе завершиться. Или же, вызов f не завершается, поскольку происходит нелокальная смена контекста вычисления, прыжок в совершенно другое место программы (если язык программирования нам предоставляет такую возможность). Грубо говоря, в какой-то момент исполнения f мы сказали: "Ой, всё" и занялись другим делом.
Что интересно, в программировании тип ⊥ обычно не встречается. Он, на самом деле, не сильно нужен, особенно если есть возможность использовать обобщенные типы. Тип ∀R R (все высказывания верны) вполне абсурден¹. Вообще, вместо специального пустого типа ⊥ можно использовать неизвестный тип R, на который не накладывается никаких ограничений. Потом его можно заменить, в том числе на пустой тип. Такую переменную R в процессе работы с ней приходится трактовать как пустой тип, поскольку мы ничего о типе R не знаем. Другое дело, что R можно заменить и на тип содержащий значения. Так что, то что мы полагаем абсурдом, на самом деле может иметь смысл. При таком подходе закон исключённого третьего имеет следующий вид:
Что интересно, в программировании тип ⊥ обычно не встречается. Он, на самом деле, не сильно нужен, особенно если есть возможность использовать обобщенные типы. Тип ∀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.
Получается, что введение 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) ‒ они позволяют эмулировать продолжения и аналогичные механизмы для части программы.
Можно сказать, что конструктивный смысл у классической логики есть, но при этом каждому классическому доказательству можно приписать несколько конструкций. Это подтверждается тем, что существует несколько алгоритмов перевода классических доказательств в конструктивные, дающие разные доказательства в результате (один из них предложен Гёделем и Генценом, существуют и другие). Разные преобразования соответствуют разным способам вычисления программы, в которой используется callcc. Кстати, такие преобразования применяются и в программировании (так называемое continuation-passing-style translation) ‒ они позволяют эмулировать продолжения и аналогичные механизмы для части программы.
Но закончим пока с логикой классической ‒ нам пора перейти к линейной логике...
¹ Для того чтоб задать такой тип, нужно работать в языке, который соответствует логике предикатов второго порядка ‒ логике, где предикаты могут быть функциями от высказываний (в отличие от логики первого порядка, где они могут зависеть только от базовых объектов). В программировании распространены языки, которые легко позволяют первое (зависимость типа от другого типа, т.е. обобщенные типы или шаблоны), и гораздо меньше распространены языки, которые позволяют второе (зависимость типа от конкретных значений, так называемые зависимые типы).
² c и callcc обозначены жирным, чтобы подчеркнуть их уникальный статус. Для них невозможно написать реализацию средствами функционального языка, их необходимо трактовать как примитивные инструкции.
