Линейная логика — это субструктурная логика, предложенная французским логиком Жаном-Ивом Жираром как усовершенствование классической и интуиционистской логики , объединяющая дуальности первой со многими конструктивными свойствами последней. [1] Хотя логика также изучалась сама по себе, в более широком смысле идеи линейной логики оказали влияние на такие области, как языки программирования , семантика игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации ), [2] а также на лингвистику , [3] особенно из-за ее акцента на ограниченности ресурсов, дуальности и взаимодействии.
Линейная логика пригодна для множества различных представлений, объяснений и интуиций. Теоретически доказательство вытекает из анализа классического секвенциального исчисления , в котором использование ( структурных правил ) сокращения и ослабления тщательно контролируется. С точки зрения эксплуатации это означает, что логическая дедукция больше не просто о постоянно расширяющемся наборе постоянных «истин», но и способе манипулирования ресурсами , которые не всегда могут быть продублированы или выброшены по желанию. С точки зрения простых денотационных моделей линейная логика может рассматриваться как уточнение интерпретации интуиционистской логики путем замены декартовых (замкнутых) категорий симметричными моноидальными (замкнутыми) категориями или интерпретации классической логики путем замены булевых алгебр на C*-алгебры . [ требуется цитата ]
Язык классической линейной логики (CLL) определяется индуктивно с помощью нотации BNF
Здесь p и p ⊥ ранжируются по логическим атомам . По причинам, которые будут объяснены ниже, связки ⊗, ⅋, 1 и ⊥ называются мультипликативами , связки &, ⊕, ⊤ и 0 называются аддитивами , а связки ! и ? называются экспоненциалами . Мы можем далее использовать следующую терминологию:
Бинарные связки ⊗, ⊕, & и ⅋ являются ассоциативными и коммутативными; 1 — единица для ⊗, 0 — единица для ⊕, ⊥ — единица для ⅋ и ⊤ — единица для &.
Каждое предложение A в CLL имеет двойственное A ⊥ , определяемое следующим образом:
Заметим, что ( -) ⊥ является инволюцией , т. е. A ⊥⊥ = A для всех предложений. A ⊥ также называется линейным отрицанием A.
Столбцы таблицы предлагают другой способ классификации связок линейной логики, называемыйполярность : связки, отрицаемые в левом столбце (⊗, ⊕, 1, 0, !), называютсяположительными, а их двойственные в правом столбце (⅋, &, ⊥, ⊤, ?) называютсяотрицательными; см. таблицу справа.
Линейная импликация не включена в грамматику связок, но определяется в CLL с помощью линейного отрицания и мультипликативной дизъюнкции, как A ⊸ B := A ⊥ ⅋ B. Связка ⊸ иногда произносится как «лоллипоп» из-за своей формы.
Один из способов определения линейной логики — это исчисление последовательностей . Мы используем буквы Γ и Δ для ранжирования списков предложений A 1 , ..., An , также называемых контекстами . Секвента помещает контекст слева и справа от турникета , записываемый как Γ Δ . Интуитивно секвента утверждает, что конъюнкция Γ влечет за собой дизъюнкцию Δ (хотя мы имеем в виду «мультипликативную» конъюнкцию и дизъюнкцию, как объясняется ниже). Жирар описывает классическую линейную логику, используя только односторонние секвенции (где левый контекст пуст), и мы следуем здесь этому более экономичному представлению. Это возможно, потому что любые посылки слева от турникета всегда можно переместить на другую сторону и дуализировать.
Теперь мы дадим правила вывода, описывающие, как строить доказательства секвенций. [4]
Во-первых, чтобы формализовать тот факт, что нас не волнует порядок предложений внутри контекста, мы добавляем структурное правило обмена :
Обратите внимание, что мы не добавляем структурные правила ослабления и сокращения, поскольку нас интересует отсутствие предложений в секвенции и количество имеющихся копий.
Далее мы добавляем начальные последовательности и разрезы :
Правило разреза можно рассматривать как способ составления доказательств, а начальные секвенции служат единицами для композиции. В определенном смысле эти правила избыточны: поскольку мы вводим дополнительные правила для построения доказательств ниже, мы будем поддерживать свойство, что произвольные начальные секвенции могут быть получены из атомарных начальных секвенций, и что всякий раз, когда секвенция доказуема, ей можно дать доказательство без разрезов. В конечном счете, это свойство канонической формы (которое можно разделить на полноту атомарных начальных секвенций и теорему об устранении разрезов , что приводит к понятию аналитического доказательства ) лежит в основе приложений линейной логики в информатике, поскольку оно позволяет использовать логику в поиске доказательств и в качестве лямбда-исчисления, учитывающего ресурсы .
Теперь мы объясним связки, дав логические правила . Обычно в секвенциальном исчислении для каждой связки задаются как «правильные правила», так и «левые правила», по сути описывая два способа рассуждения о предложениях, включающих эту связку (например, верификацию и фальсификацию). В одностороннем представлении вместо этого используется отрицание: правые правила для связки (скажем, ⅋) фактически играют роль левых правил для ее дуала (⊗). Таким образом, мы должны ожидать определенной «гармонии» между правилом(ами) для связки и правилом(ами) для ее дуала.
Правила мультипликативной конъюнкции (⊗) и дизъюнкции (⅋):
и для их подразделений:
Обратите внимание, что правила мультипликативной конъюнкции и дизъюнкции допустимы для простой конъюнкции и дизъюнкции в классической интерпретации (т.е. они являются допустимыми правилами в LK ).
Правила для аддитивной конъюнкции (&) и дизъюнкции (⊕):
и для их подразделений:
Обратите внимание, что правила для аддитивной конъюнкции и дизъюнкции снова допустимы в классической интерпретации. Но теперь мы можем объяснить основу для мультипликативного/аддитивного различия в правилах для двух различных версий конъюнкции: для мультипликативной связки (⊗) контекст заключения ( Γ, Δ ) разделен между посылками, тогда как для аддитивной падежной связки (&) контекст заключения ( Γ ) переносится целиком в обе посылки.
Экспоненты используются для предоставления контролируемого доступа к ослаблению и сокращению. В частности, мы добавляем структурные правила ослабления и сокращения для ? 'd предложений: [5]
и используйте следующие логические правила, в которых ?Γ обозначает список предложений, каждое из которых начинается с ? :
Можно заметить, что правила для экспонент следуют иному образцу, чем правила для других связок, напоминая правила вывода, управляющие модальностями в формализаций секвенциального исчисления нормальной модальной логики S4 , и что больше нет такой четкой симметрии между дуалами ! и ? . Эта ситуация исправляется в альтернативных представлениях CLL (например, представление LU).
Помимо описанных выше двойственностей Де Моргана , в линейной логике существуют некоторые важные эквивалентности:
По определению A ⊸ B как A ⊥ ⅋ B последние два закона дистрибутивности также дают:
(Здесь A ≣ B есть ( A ⊸ B ) & ( B ⊸ A ) .)
Отображение, которое не является изоморфизмом, но играет решающую роль в линейной логике:
Линейные распределения являются фундаментальными в теории доказательств линейной логики. Последствия этого отображения были впервые исследованы в [6] и названы «слабым распределением». В последующей работе оно было переименовано в «линейное распределение», чтобы отразить фундаментальную связь с линейной логикой.
Следующие формулы дистрибутивности в общем случае не являются эквивалентностью, а лишь следствием:
Как интуиционистская, так и классическая импликация могут быть восстановлены из линейной импликации путем вставки экспонент: интуиционистская импликация кодируется как ! A ⊸ B , в то время как классическая импликация может быть кодирована как !? A ⊸ ? B или ! A ⊸ ?! B (или множество альтернативных возможных переводов). [7] Идея заключается в том, что экспоненты позволяют нам использовать формулу столько раз, сколько нам нужно, что всегда возможно в классической и интуиционистской логике.
Формально существует перевод формул интуиционистской логики в формулы линейной логики таким образом, что гарантируется, что исходная формула доказуема в интуиционистской логике тогда и только тогда, когда переведенная формула доказуема в линейной логике. Используя отрицательный перевод Гёделя–Гентцена , мы можем таким образом встроить классическую логику первого порядка в линейную логику первого порядка.
Лафонт (1993) впервые показал, как интуиционистская линейная логика может быть объяснена как логика ресурсов, тем самым предоставляя логическому языку доступ к формализмам, которые могут быть использованы для рассуждений о ресурсах внутри самой логики, а не, как в классической логике, посредством нелогических предикатов и отношений. Классический пример Тони Хоара (1985) с торговым автоматом может быть использован для иллюстрации этой идеи.
Предположим, что мы представляем наличие шоколадного батончика атомарным предложением конфета , а наличие доллара — $1 . Чтобы заявить о том, что за доллар можно купить один шоколадный батончик, мы могли бы записать импликацию $1 ⇒ конфета . Но в обычной (классической или интуиционистской) логике из A и A ⇒ B можно заключить A ∧ B . Таким образом, обычная логика приводит нас к убеждению, что мы можем купить шоколадный батончик и сохранить свой доллар! Конечно, мы можем избежать этой проблемы, используя более сложные кодировки, [ необходимо разъяснение ] хотя обычно такие кодировки страдают от проблемы фрейма . Однако отказ от ослабления и сжатия позволяет линейной логике избегать такого рода ложных рассуждений даже с «наивным» правилом. Вместо $1 ⇒ конфета мы выражаем свойство торгового автомата как линейную импликацию $1 ⊸ конфета . Из $1 и этого факта можно сделать вывод candy , но не $1 ⊗ candy . В общем случае мы можем использовать линейное логическое предложение A ⊸ 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 ⊸ ( конфеты ⊗ чипсы ⊗ напиток ) из этого.
Представленные Жаном-Ивом Жираром сети доказательств были созданы для того, чтобы избежать бюрократии , то есть всего того, что делает два вывода различными с логической точки зрения, но не с «моральной» точки зрения.
Например, эти два доказательства «морально» идентичны:
Целью корректурных сеток является обеспечение их идентичности путем создания их графического представления.
Отношение вывода в полном CLL неразрешимо . [8] При рассмотрении фрагментов CLL проблема принятия решения имеет различную сложность:
Множество вариаций линейной логики возникают путем дальнейшей доработки структурных правил:
Были рассмотрены различные интуиционистские варианты линейной логики. При использовании однозаключительного секвенциального исчисления, как в ILL (интуиционистская линейная логика), связки ⅋, ⊥ и ? отсутствуют, а линейная импликация рассматривается как примитивная связка. В FILL (полная интуиционистская линейная логика) связки ⅋, ⊥ и ? присутствуют, линейная импликация является примитивной связкой и, подобно тому, что происходит в интуиционистской логике, все связки (кроме линейного отрицания) независимы. Существуют также расширения линейной логики первого и более высокого порядка, формальное развитие которых является в некоторой степени стандартным (см. логику первого порядка и логику высшего порядка ).
Медиа, связанные с линейной логикой на Wikimedia Commons
