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

Линейная логика - это субструктурная логика, предложенная Жан-Ивом Жираром как уточнение классической и интуиционистской логики , объединяющая дуальности первой со многими конструктивными свойствами последней. ^[1] Хотя логика также изучалась сама по себе, в более широком смысле идеи линейной логики оказали влияние на такие области, как языки программирования , семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой логики). теория информации ), ^[2], а такжелингвистика , ^[3] в частности , из - за его акцент на ресурсы ограниченности, двойственность и взаимодействии.

Линейная логика поддается множеству различных представлений, объяснений и интуиций. Теоретически это доказательство вытекает из анализа классического секвенциального исчисления, в котором использование ( структурных правил ) сжатия и ослабления тщательно контролируется. С практической точки зрения это означает, что логическая дедукция - это уже не просто постоянно расширяющаяся коллекция устойчивых «истин», но также способ манипулирования ресурсами, которые не всегда могут быть скопированы или выброшены по желанию. В терминах простых денотационных моделей линейная логика может рассматриваться как уточнение интерпретации интуиционистской логики путем замены декартовых (закрытых) категорийс помощью симметричных моноидального (закрытых) категорий или интерпретации классической логики, заменяя булевы алгебры с помощью C * -алгебры . ^{[ необходима цитата ]}

Связи, двойственность и полярность [ править ]

Синтаксис [ править ]

Язык классической линейной логики (CLL) определяется индуктивно с помощью обозначения BNF

Здесь р и р ^⊥ пробегают логические атомы . По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и ⊥ называются мультипликативными , связки &, ⊕, ⊤ и 0 называются аддитивными , а связки! а также ? называются экспонентами . В дальнейшем мы можем использовать следующую терминологию:

Бинарные связки ⊗, ⊕, & и ⅋ ассоциативны и коммутативны; 1 - единица для, 0 - единица для, ⊥ - единица для, ⊤ - единица для &.

Каждое предложение A в CLL имеет двойственный A ^⊥ , определяемый следующим образом:

Заметим , что (-) ^⊥ является инволюцией , т.е. ^⊥⊥ = для всех предложений. ^⊥ также называется линейное отрицание из A .

Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемый полярностью : связки, отрицаемые в левом столбце (⊗, ⊕, 1, 0,!), Называются положительными , а их двойственные справа (⅋, &, ⊥, ⊤,?) Называются отрицательными ; ср. таблица справа.

Линейный вывод не входит в грамматике связок, но определим в CLL с использованием линейной отрицании и мультипликативной дизъюнкции, от A ⊸ B  : = ^⊥ ⅋ Б . Соединительный элемент ⊸ иногда произносится как « леденец » из-за его формы.

Представление последовательного исчисления [ править ]

Один из способов определения линейной логики - это последовательное исчисление . Мы используем буквы Γ и ∆, чтобы пробегать по списку предложений A ₁ , ..., A _n , также называемых контекстами . Секвенции помещают контекст слева и справа от турникета , написанного Г Д${\displaystyle \vdash }$ . Интуитивно секвенция утверждает, что конъюнкция Γ влечет за собой дизъюнкцию ∆ (хотя мы имеем в виду «мультипликативную» конъюнкцию и дизъюнкцию, как объясняется ниже). Жирар описывает классическую линейную логику, используя только одностороннююsequents (где левый контекст пуст), и мы следуем здесь более экономичному представлению. Это возможно потому, что любое помещение слева от турникета всегда можно переместить на другую сторону и сдвоить.

Теперь мы дадим правила вывода, описывающие, как строить доказательства секвенций. ^[4]

Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правило обмена :

${\displaystyle \vdash }$Γ, A 1 , A 2 , Δ

${\displaystyle \vdash }$Γ, A 2 , A 1 , Δ

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

Затем мы добавляем начальные секвенции и разрезы :

${\displaystyle \vdash }$ А , А ⊥

${\displaystyle \vdash }$Γ, A       ${\displaystyle \vdash }$ А ⊥ , Δ ${\displaystyle \vdash }$ Γ, Δ

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

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

Множители [ править ]

Правила мультипликативной конъюнкции (⊗) и дизъюнкции (⅋):

${\displaystyle \vdash }$Γ, A       ${\displaystyle \vdash }$Δ, B ${\displaystyle \vdash }$Γ, Δ, A ⊗ B

${\displaystyle \vdash }$Γ, A , B ${\displaystyle \vdash }$Γ, A ⅋ B

и для их агрегатов:

${\displaystyle \vdash }$ 1

${\displaystyle \vdash }$ Γ ${\displaystyle \vdash }$ Γ, ⊥

Заметьте, что правила мультипликативной конъюнкции и дизъюнкции допустимы для простой конъюнкции и дизъюнкции в классической интерпретации (т. Е. Они допустимые правила в LK ).

Добавки [ править ]

Правила аддитивной конъюнкции (&) и дизъюнкции (⊕):

${\displaystyle \vdash }$Γ, A       ${\displaystyle \vdash }$Γ, B ${\displaystyle \vdash }$Γ, A и B

${\displaystyle \vdash }$Γ, A ${\displaystyle \vdash }$Γ, A ⊕ B

${\displaystyle \vdash }$Γ, B ${\displaystyle \vdash }$Γ, A ⊕ B

и для их агрегатов:

${\displaystyle \vdash }$ Γ, ⊤

(нет правила для 0 )

Заметим, что правила аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу мультипликативного / аддитивного различия в правилах для двух разных версий конъюнкции: для мультипликативной связки (⊗) контекст заключения ( Γ, ∆ ) разбивается между предпосылками, тогда как для связки аддитивного случая (&) контекст заключения ( Γ ) целиком переносится в обе посылки.

Экспоненты [ править ]

Экспоненты используются для предоставления контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сжатия для предложений? ^[5]

${\displaystyle \vdash }$ Γ ${\displaystyle \vdash }$Γ,? А

${\displaystyle \vdash }$Γ,? А ,? А ${\displaystyle \vdash }$Γ,? А

и используйте следующие логические правила:

${\displaystyle \vdash }$? Γ, A ${\displaystyle \vdash }$? Γ,! А

${\displaystyle \vdash }$Γ, A ${\displaystyle \vdash }$Γ,? А

Можно заметить, что правила для экспонент следуют шаблону, отличному от правил для других связок, напоминая правила вывода, управляющие модальностями в формализации секвенциального исчисления нормальной модальной логики S4, и что больше нет такой четкой симметрии между двойники! а также ?. Эта ситуация исправляется в альтернативных представлениях CLL (например, в представлении LU ).

Замечательные формулы [ править ]

В дополнение к двойственности Де Моргана, описанной выше, некоторые важные эквивалентности в линейной логике включают:

Распределительность

По определению A ⊸ B как A ^⊥ ⅋ B последние два закона дистрибутивности также дают:

(Здесь A ≣ B означает ( A ⊸ B ) & ( B ⊸ A ) .)

Экспоненциальный изоморфизм

Линейные распределения

Карта, которая не является изоморфизмом, но играет решающую роль в линейной логике:

Линейные распределения являются фундаментальными в теории доказательств линейной логики. Следствия этого отображения были впервые исследованы в ^[6] и названы «слабым распределением». В последующей работе оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.

Другие последствия

Следующие формулы дистрибутивности в общем случае не эквивалентны, а только импликации:

Кодирование классической / интуиционистской логики в линейной логике [ править ]

Как интуиционистская, так и классическая импликация могут быть восстановлены из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как ! A ⊸ B , а классическая импликация может быть закодирована как !? А ⊸? B или ! А ⊸?! B (или множество альтернативных возможных переводов). ^[7] Идея состоит в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.

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

Интерпретация ресурса [ править ]

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

Предположим, что мы представляем конфету с помощью атомарной конфетки , а доллар - с помощью 1 доллара . Чтобы констатировать тот факт, что за доллар можно купить один шоколадный батончик, мы могли бы написать импликацию $ 1 ⇒ конфеты . Но в обычной (классической или интуиционистской) логики, от A и A ⇒ B можно заключить A ∧ B . Итак, обычная логика приводит нас к мысли, что мы можем купить шоколадный батончик и сохранить свои деньги! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки, ^{[ требуется пояснение ],} хотя обычно такие кодировки страдают отпроблема с рамкой . Однако отказ от ослабления и сжатия позволяет линейной логике избегать такого рода ложных рассуждений даже с «наивным» правилом. Вместо $ 1 ⇒ конфеты , мы выражаем собственность торгового автомата в качестве линейного следования $ 1 ⊸ конфеты . От $ 1 и этот факт, мы можем заключить , конфеты , но не $ 1 ⊗ конфеты . В общем, мы можем использовать линейное логическое суждение ⊸ B , чтобы выразить законность преобразования ресурса A в ресурсе B .

На примере торгового автомата рассмотрим «ресурсные интерпретации» других мультипликативных и аддитивных связок. (Экспоненты предоставляют средства для объединения этой ресурсной интерпретации с обычным понятием постоянной логической истины .)

Мультипликативная конъюнкция ( A ⊗ B ) обозначает одновременное появление ресурсов, которые будут использоваться в соответствии с указаниями потребителя. Например, если вы покупаете палку резины и бутылку безалкогольного напитка, то вы запрашиваете камеди ⊗ напиток . Константа 1 обозначает отсутствие какого-либо ресурса и, таким образом, функционирует как единица измерения.

Аддитивная конъюнкция ( A & B ) представляет собой альтернативное появление ресурсов, выбор которых контролирует потребитель. Если в торговом автомате есть пачка чипсов, шоколадный батончик и банка безалкогольных напитков, каждая из которых стоит один доллар, то по этой цене вы можете купить ровно один из этих продуктов. Таким образом , мы пишем $ 1 ⊸ ( конфеты & чипсы & напиток ) . Мы не пишем $ 1 ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) , что означало бы, что одного доллара достаточно для покупки всех трех продуктов вместе. Однако от $ 1⊸ ( конфеты и чипсы и напитки ) , мы можем правильно вывести $ 3 ⊸ ( конфеты ⊗ чипы ⊗ напиток ) , где $ 3  : = $ 1 ⊗ $ 1 ⊗ $ 1 . Блок аддитивной связи можно рассматривать как мусорную корзину для ненужных ресурсов. Например, мы можем написать $ 3 ⊸ ( конфеты ⊗ ⊤), чтобы выразить, что с тремя долларами вы можете получить шоколадный батончик и некоторые другие вещи, не вдаваясь в подробности (например, чипсы и напиток, или 2 доллара, или 1 доллар и чипсы. , так далее.).

Аддитивная дизъюнкция ( A ⊕ B ) представляет собой альтернативное вхождение ресурсов, выбор которых контролирует машина. Например, предположим, что торговый автомат разрешает азартные игры: вставьте доллар, и автомат может выдать шоколадный батончик, пачку чипсов или безалкогольный напиток. Мы можем выразить эту ситуацию как $ 1 ⊸ ( конфеты ⊕ чипсы ⊕ напиток ) . Константа 0 представляет продукт, который невозможно произвести, и, таким образом, служит единицей ⊕ (машина, которая может производить A или 0 , так же хороша, как машина, которая всегда производит Aпотому что ему никогда не удастся произвести 0). Таким образом , в отличие от выше, мы не можем вывести $ 3 ⊸ ( конфеты ⊗ Щепа ⊗ напиток ) от этого.

Мультипликативная дизъюнкция ( ⅋ Б ) более трудно глянец с точкой зрения интерпретации ресурса, хотя мы можем кодировать обратно в линейную импликацию, либо как A ^⊥ ⊸ B или B ^⊥ ⊸ A .

Другие системы доказательств [ править ]

Доказательные сети [ править ]

Представленные Жан-Ивом Жираром , сети доказательств были созданы, чтобы избежать бюрократии , то есть всего того, что делает два вывода разными с логической точки зрения, но не с «моральной» точки зрения.

Например, эти два доказательства идентичны «морально»:

${\displaystyle \vdash }$ А , Б , В , D ${\displaystyle \vdash }$ A ⅋ B , C , D ${\displaystyle \vdash }$ A ⅋ B , C ⅋ D

${\displaystyle \vdash }$ А , Б , В , D ${\displaystyle \vdash }$ А , Б , В ⅋ D ${\displaystyle \vdash }$ A ⅋ B , C ⅋ D

Цель сетей доказательства - сделать их идентичными, создав их графическое представление.

Семантика [ править ]

Алгебраическая семантика [ править ]

Разрешимость / сложность вывода [ править ]

Отношение следования в полной CLL неразрешимо . ^[8] При рассмотрении фрагментов CLL проблема решения имеет разную сложность:

• Мультипликативная линейная логика (MLL): только мультипликативные связки. Вывод MLL является NP-полным , даже ограничиваясь предложениями Хорна в чисто импликативном фрагменте ^[9] или безатомными формулами. ^[10]
• Мультипликативно-аддитивная линейная логика (MALL): только мультипликативные и аддитивные (т. Е. Без экспоненциальной зависимости). ТОРГОВЫЙ ВЕЩАНИЕ является PSPACE-полным . ^[8]
• Мультипликативно-экспоненциальная линейная логика (MELL): только мультипликативы и экспоненты. Путь восстановления от проблемы достижимости для сетей Петри , ^[11] MELL Воплощение должно быть , по крайней мере EXPSPACE твердолобого , хотя разреши сам имел статус давнишней открытой проблемы. В 2015 году доказательство распознаваемости была опубликована в журнале ТКС , ^[12] , но позже было показано , что ошибочными. ^[13]
• В 1995 году было показано, что аффинная линейная логика (то есть линейная логика с ослаблением, расширение, а не фрагмент) разрешима ^[14].

Варианты [ править ]

Многие вариации линейной логики возникают в результате дальнейшего изменения структурных правил:

• Аффинная логика , запрещающая сжатие, но допускающая глобальное ослабление (разрешимое расширение).
• Строгая логика или соответствующая логика , запрещающая ослабление, но допускающая глобальное сокращение.
• Некоммутативная логика или упорядоченная логика, которая удаляет правило обмена в дополнение к запрету ослабления и сжатия. В упорядоченной логике линейная импликация подразделяется на левую и правую.

Рассмотрены различные интуиционистские варианты линейной логики. Если основано на представлении последовательного исчисления с одним выводом, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и? отсутствуют, и линейная импликация рассматривается как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и? присутствуют, линейная импликация является примитивной связкой, и, подобно тому, что происходит в интуиционистской логике, все связки (кроме линейного отрицания) независимы. Существуют также расширения первого и более высокого порядка линейной логики, формальное развитие которых в некоторой степени стандартно (см. Логику первого и высшего порядка ).

См. Также [ править ]

• Система типов Линейной , A субструктурного типа системы
• Логика единства (LU)
• Доказательные сети
• Геометрия взаимодействия
• Семантика игры
• Интуиционистская логика
• Логика вычислимости
• Ludics
• Пространства Чу
• Тип уникальности
• Программирование линейной логики

Ссылки [ править ]

Дальнейшее чтение [ править ]

• Жирар, Жан-Ив. Линейная логика , Теоретическая информатика, Том 50, № 1, стр. 1–102, 1987.
• Жирар, Жан-Ив, Лафон, Ив и Тейлор, Поль. Доказательства и типы . Кембриджская пресса, 1989.
• Хоар, ЦАР, 1985. Связь последовательных процессов . Prentice-Hall International. ISBN 0-13-153271-5 
• Лафон, Ив, 1993. Введение в линейную логику . Конспект лекций Летней школы TEMPUS по алгебраическим и категориальным методам в компьютерных науках , Брно, Чешская Республика.
• Трельстра А.С. Лекции по линейной логике . CSLI (Центр изучения языка и информации) Конспект лекций № 29. Стэнфорд, 1992.
• AS Troelstra , Х. Швихтенберг (1996). Основная теория доказательств . В серии « Кембриджские трактаты по теоретической информатике» , издательство Кембриджского университета, ISBN 0-521-77911-1 . 
• Ди Космо, Роберто, и Данос, Винсент. Учебник по линейной логике .
• Введение в линейную логику (постскриптум) Патрика Линкольна
• Введение в линейную логику Торбена Браунера
• Вкус линейной логики Филипа Вадлера
• Линейная логика от Roberto Di Cosmo и Дейл Миллер . Стэнфордская энциклопедия философии (издание осень 2006 г.), Эдвард Н. Залта (ред.).
• Обзор линейной логики программирования по Дейл Миллер . В « Линейной логике в компьютерных науках» под редакцией Эрхарда, Жирара, Рюэ и Скотта. Издательство Кембриджского университета. Конспект лекций Лондонского математического общества, том 316, 2004 г.
• Линейная логика вики

Внешние ссылки [ править ]

• СМИ, связанные с линейной логикой на Викискладе?
• Программа для доказательства линейной логики , доступная для использования в Интернете по адресу : Naoyuki Tamura / Dept of CS / Kobe University / Japan