суббота, 21 февраля 2015 г.

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

One is the loneliest number that you'll ever do 
Two can be as bad as one 
It's the loneliest number since the number one
«One», Harry Nilsson 

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

Брауэр считал, что математика — это особый, доязыковой вид деятельности нашего разума, который заключается в конструировании и изучении свойств абстрактных объектов, в первую очередь натуральных чисел. Как особый вид деятельности математика не нуждается в сведении к формальной логике, хотя таковая и является частью математики. Впрочем, к логике бездумно применённой к бесконечным наборам объектов у него были претензии. Пусть, например, мы показали, что ¬∀x ¬P(x). Согласно классической логике это означает, что  x P(x). И если x принимает конечное число значений, то проверив их по очереди, мы сможем найти требуемый. Но если x может принимать неограниченное количество значений, то мы не вправе говорить, что требуемый объект существует, поскольку мы не можем в этом удостоверится напрямую.

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

Оппонентом Брауэра стал Давид Гильберт. "Никому не удастся изгнать математиков из Рая", говорил он. Не принимая и логицизм, Гильберт боялся за судьбу математического знания  если следовать конструктивному подходу, то многие из теорем, например, мат. анализа придётся выкинуть. Не желая ничего выкидывать, Гильберт затеял программу спасения математики  выделить содержательное ядро, метаматематику, в которой приемлемы только финитные методы, остальную же математику формализовать, свести к игре символами, и эту игру изучать в рамках содержательной математики, с целью показать непротиворечивость такой игры. Из попытки эту программу реализовать родилась computer science; деятельность  Чёрча, Тюринга, Гёделя, Клини напрямую связана с реализацией этой программы.

Брауэру формалистский подход Гильберта был неинтересен. "Ложная теория, не натолкнувшаяся на противоречие, не становится от этого менее ложной", утверждал он. Также, его не интересовало формальное изложение логики интуционистской математики. Но его ученики были свободны от несколько мистических взглядов учителя, и Аренд Хейтинг формализовал интуиционистскую логику. Она не сильно отличалась от классической, в ней просто отсутствовал закон исключенного третьего и его аналоги, а также правило отрицания для кванторов.

Но что значит интуиционистская логика? Для логики классической известны модели, в том числе конечные. Интуиционистская логика кажется уродливой по сравнению с классической, без столь симметричных правил де Моргана. Есть ли у неё собственные модели? Интерпретация интуиционистской логики была представлена Хейтингом и независимо от него А. Н. Колмогоровым. По давней математической традиции, именованные определения должны содержать имя математика, не имеющего отношения к определению. Интерпретация носит имена Брауэра — Хейтинга — Колмогорова (сокращенно BHK).

В чём же она заключалась? Как уже было замечено, интуиционисты по-другому трактуют связку или и квантор существования  они требуют чтобы, доказательство утверждения A или B содержало указание на то, в каких случаях выполняется A, а в каких B, а доказательство утверждения "существует  x такой что...", давало ответ, как найти такой xТакой подход можно обобщить, поменяв смысл "утверждать, что высказывание верно". В интерпретации BHK нельзя ничего утверждать, не предоставив свидетельство. С каждым высказыванием сопоставляется набор свидетельств его истинности. Ложное высказывание не имеет свидетельств в свою пользу. Чтобы определить логические связки достаточно указать, какой объект мы ожидаем получить в качестве свидетельства истинности. Отношение "a свидетельствует об A" обозначим a : A. Кроме того, логические связки с поведением отличным от классического стоит иначе обозначать. Это другое "или", другой квантор существования, с точки зрения интуициониста более сильные нежели их классические варианты. Конструктивные аналоги обозначим так:

A + B  конструктивное или
P(x конструктивное существует
⇒  конструктивное следует

Тогда интуиционистские логические связки можно определить так:
  • ⋀  свидетельством служит пара (a,b), где a : A,  b : B
  • A + B  свидетельством служит пара (l, a) или (r, b), где a : A, b : B, а l и r — теги, определяющие, какое из высказываний A, B полагается верным
  •  B — свидетельством служит алгоритм, по которому можно из a : A получить b : B 
  • ¬ свидетельством служит алгоритм, по которому можно из a : A получить свидетельство абсурдного высказывания. Если обозначить ⊥ некое ложное высказывание, то  ¬A  можно определить как A ⇒ ⊥
  • x P(x свидетельством служит алгоритм, по которому можно из x получить p : P(x)
  • P(x свидетельством служит пара (x, p), где для х выполняется P(x), а p является свидетельством этого 
Таким образом, конструктивное доказательство утверждения есть описание конструирования объекта, подтверждающего это утверждение.

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

Хотелось бы еще обратить внимание на операцию следования. Её классический вариант никак не связывает причину и следствие, интуиционистское следование чуть более релевантно — требуется алгоритм, по которому можно перейти от причины к следствию. Ничего, правда, не сказано про то, должен ли алгоритм использовать причину при построении следствия. В линейной логике такое требование налагается, но всему своё время. 

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


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

среда, 18 февраля 2015 г.

Линейная Логика 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)

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

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

среда, 11 февраля 2015 г.

Линейная логика I

Линейная логика вспомнилась мне, когда я разбирался с rvalue-ссылками в C++11. Не то чтобы новый тип ссылок имеет много общего с линейной логикой, но некоторые аспекты схожи. Добавление rvalue-ссылок - это попытка разграничить в языке значения долгоживущие и временные, а также предоставить способ поглощать значения временные, используя их внутреннюю структуру для новых значений. 

Для программистов на C++ эффективная работа с временными значениями нужна, во-первых, потому что эффективность работы программы ставится во главу угла разработчиками языка, во-вторых, потому что это позволяет писать код естественным образом - так, чтобы результат операции был выражен её возвращаемым значением, даже если это вектор с кучей значений внутри - теперь такой естественный стиль является также эффективным, что приятно. 

Люди, которые разрабатывали rvalue-ссылки, правда, немного намудрили с дизайном - и теперь даже для того чтобы разобраться, где собственно rvalue-ссылка, а где нет, нужен некоторый навык. Но это у них так принято.

Что же общего у линейной логики и нового C++? Формальная логика обычно представляется системой оперирующей высказываниями, для которых мы можем установить их истинность (или ложность). Как правило, речь идет о высказываниях, для которых истинность может быть установлена раз и навсегда. Это величина константная и вечная. Высказывание нельзя потратить, израсходовать. Но для линейной логики это не совсем так. Она имеет дело как с высказываниями, так и с командами/действиями. Единожды совершённое действие не обязательно можно повторить. Таким образом, в линейной логике наличествуют величины расходуемые, временные.

На C++ линейная логика, по всей видимости, не оказала влияния. Но некоторые языки программирования, вышедшие из академической среды, явно или неявно используют концепции, вдохновлённые линейной логикой. Считается, что для самих логиков эта формальная система не столь важна, как для computer science.

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

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