Связанная логика

Связанная логика [1] является разновидностью субструктурной логики, предложенной Питером О'Хирном и Дэвидом Пимом. Связанная логика предоставляет примитивы для рассуждений о составе ресурсов , которые помогают в композиционном анализе компьютерных и других систем. Она имеет категориально-теоретическую и истинностно-функциональную семантику, которую можно понять в терминах абстрактной концепции ресурса, и теорию доказательств, в которой контексты Γ в суждении вывода Γ ⊢ A являются древовидными структурами (связками), а не списками или ( мульти ) множествами, как в большинстве исчислений доказательств . Связанная логика имеет связанную теорию типов , и ее первое применение заключалось в предоставлении способа управления наложением имен и другими формами помех в императивных программах . [2] Логика нашла дальнейшее применение в верификации программ , где она является основой языка утверждений логики разделения , [3] и в моделировании систем , где она предоставляет способ разложения ресурсов, используемых компонентами системы. [4] [5] [6]

Фонды

Теорема дедукции классической логики связывает конъюнкцию и импликацию:

А ∧ Б ⊢ С если да А ⊢ Б ⇒ С {\displaystyle A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C}

В связной логике есть две версии теоремы дедукции:

А ∗ Б ⊢ С если да А ⊢ Б − ∗ С а также А ∧ Б ⊢ С если да А ⊢ Б ⇒ С {\displaystyle A*B\vdash C\quad {\mbox{если и только тогда}}\quad A\vdash B{-\!\!*}C\qquad {\mbox{и также}}\qquad A\wedge B\vdash C\quad {\mbox{если и только тогда}}\quad A\vdash B\Rightarrow C}

А ∗ Б {\displaystyle А*Б} и являются формами конъюнкции и импликации, которые учитывают ресурсы (объясняется ниже). В дополнение к этим связкам сгруппированная логика имеет формулу, иногда записываемую как I или emp, которая является единицей *. В оригинальной версии сгруппированной логики и были связками из интуиционистской логики , в то время как булев вариант берет и (и ) как из традиционной булевой логики . Таким образом, сгруппированная логика совместима с конструктивными принципами, но никоим образом не зависит от них. Б − ∗ С {\displaystyle B{-\!\!*}C} ∧ {\displaystyle \клин} ⇒ {\displaystyle \Стрелка вправо} ∧ {\displaystyle \клин} ⇒ {\displaystyle \Стрелка вправо} ¬ {\displaystyle \отрицательный}

Истинно-функциональная семантика (семантика ресурсов)

Самый простой способ понять эти формулы — с точки зрения их истинностно-функциональной семантики. В этой семантике формула является истинной или ложной относительно заданных ресурсов. утверждает, что имеющийся ресурс может быть разложен на ресурсы, которые удовлетворяют и . говорит, что если мы скомпонуем имеющийся ресурс с дополнительным ресурсом, который удовлетворяет , то объединенный ресурс удовлетворяет . и имеют их знакомые значения. А ∗ Б {\displaystyle А*Б} А {\displaystyle А} Б {\displaystyle Б} Б − ∗ С {\displaystyle B{-\!\!*}C} Б {\displaystyle Б} С {\displaystyle С} ∧ {\displaystyle \клин} ⇒ {\displaystyle \Стрелка вправо}

Основой для такого прочтения формул послужила семантика принуждения, предложенная Пимом, где отношение принуждения означает « A удерживает ресурс r » . Семантика аналогична семантике интуиционистской или модальной логики Крипке , но элементы модели рассматриваются как ресурсы, которые могут быть составлены и разложены, а не как возможные миры, которые доступны друг из друга. Например, семантика принуждения для конъюнкции имеет вид г ⊨ А {\displaystyle r\models A}

г ⊨ А ∗ Б если да ∃ г А г Б . г А ⊨ А , г Б ⊨ Б , и г А ∙ г Б ≤ г {\displaystyle r\models A*B\quad {\mbox{если и только если}}\quad \существует r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{и}}\,r_{A}\bullet r_{B}\leq r}

где — способ объединения ресурсов, — отношение аппроксимации. г А ∙ г Б {\displaystyle r_{A}\bullet r_{B}} ≤ {\displaystyle \leq}

Эта семантика сгруппированной логики опирается на предыдущие работы в области релевантной логики (особенно на операциональную семантику Раутли–Мейера), но отличается от нее тем, что не требует и , принимая семантику стандартных интуиционистских или классических версий и . Свойство оправдано при размышлении о релевантности, но отрицается соображениями ресурса; наличие двух копий ресурса не то же самое, что наличие одной, и в некоторых моделях (например, моделях кучи ) может даже не быть определено. Стандартная семантика (или отрицания) часто отвергается релевантистами в их попытке избежать «парадоксов материальной импликации», которые не являются проблемой с точки зрения моделирования ресурсов и, следовательно, не отвергаются сгруппированной логикой. Семантика также связана с «фазовой семантикой» линейной логики , но снова отличается принятием стандартной (даже булевой) семантики и , которая в линейной логике отвергается в попытке быть конструктивной. Эти соображения подробно обсуждаются в статье о семантике ресурсов, написанной Пимом, О'Хирном и Янгом. [7] г ∙ г ≤ г {\displaystyle r\bullet r\leq r} ∧ {\displaystyle \клин} ⇒ {\displaystyle \Стрелка вправо} г ∙ г ≤ г {\displaystyle r\bullet r\leq r} г ∙ г {\displaystyle r\пуля r} ⇒ {\displaystyle \Стрелка вправо} ∧ {\displaystyle \клин} ⇒ {\displaystyle \Стрелка вправо}

Категориальная семантика (дважды замкнутые категории)

Двойная версия теоремы дедукции сгруппированной логики имеет соответствующую теоретико-категорную структуру. Доказательства в интуиционистской логике могут быть интерпретированы в декартовых замкнутых категориях, то есть категориях с конечными произведениями, удовлетворяющими ( естественному в A и C ) соответствию сопряжения , связывающему hom-множества:

ЧАС о м ( А ∧ Б , С ) изоморфен ЧАС о м ( А , Б ⇒ С ) {\displaystyle Hom(A\wedge B,C)\quad {\mbox{изоморфен}}\quad Hom(A,B\Rightarrow C)}

Связанную логику можно интерпретировать в категориях, имеющих две такие структуры

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

Множество категориальных моделей может быть задано с использованием конструкции тензорного произведения Дэя . [8] Кроме того, импликативный фрагмент сгруппированной логики получил игровую семантику . [9]

Алгебраическая семантика

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

Алгебраическая модель сгруппированной логики — это частично упорядоченное множество, которое является алгеброй Гейтинга и которое несет дополнительную коммутативную резидуальную решетчатую структуру (для той же решетки, что и алгебра Гейтинга): то есть упорядоченный коммутативный моноид с ассоциированной импликацией, удовлетворяющей . А ∗ Б ≤ С если да А ≤ Б − ∗ С {\displaystyle A*B\leq C\quad {\mbox{iff}}\quad A\leq B{-\!\!*}C}

Булева версия групповой логики имеет следующие модели.

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

Теория доказательств и теория типов (группы)

Исчисление доказательств сгруппированной логики отличается от обычных исчислений последовательностей наличием древовидного контекста гипотез вместо плоской структуры, подобной списку. В его теориях доказательств, основанных на последовательностях, контекст в суждении о выводе представляет собой конечное корневое дерево, листья которого являются предложениями, а внутренние узлы помечены способами композиции, соответствующими двум конъюнкциям. Два оператора объединения, запятая и точка с запятой, используются (например) в правилах введения для двух импликаций. Δ {\displaystyle \Дельта} Δ ⊢ А {\displaystyle \Дельта \vdash А}

Г , А ⊢ Б Г ⊢ А − ∗ Б Г ; А ⊢ Б Г ⊢ А ⇒ Б {\displaystyle {\frac {\Gamma ,A\vdash B}{\Gamma \vdash A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;A\vdash B}{\Gamma \vdash A{\Rightarrow }B}}}

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

  • Мультипликативная композиция отрицает структурные правила ослабления и сжатия. Δ , Г {\displaystyle \Дельта,\Гамма}
  • Состав добавки допускает ослабление и усадку целых пучков. Δ ; Г {\displaystyle \Дельта;\Гамма}

Структурные правила и другие операции над группами часто применяются глубоко внутри древовидного контекста, а не только на верхнем уровне: таким образом, это в некотором смысле исчисление глубокого вывода .

Связанной логике соответствует теория типов, имеющая два вида типа функции. Следуя соответствию Карри–Ховарда , правила введения для импликаций соответствуют правилам введения для типов функций.

Г , х : А ⊢ М : Б Г ⊢ λ х . М : А − ∗ Б Г ; х : А ⊢ М : Б Г ⊢ α х . М : А ⇒ Б {\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda xM:A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;x:A\vdash M:B}{\Gamma \vdash \alpha xM:A{\Rightarrow }B}}}

Здесь есть два отдельных связующих элемента, и , по одному для каждого типа функции. λ {\displaystyle \лямбда} α {\displaystyle \альфа}

Теория доказательств сгруппированной логики исторически обязана использованием связок в релевантной логике. [10] Но сгруппированная структура может быть в некотором смысле выведена из категориальной и алгебраической семантики: чтобы сформулировать правило введения для мы должны имитировать слева в секвенциях, а чтобы ввести мы должны имитировать . Это соображение приводит к использованию двух объединяющих операторов. − ∗ {\displaystyle {-\!\!*}} ∗ {\displaystyle *} ⇒ {\displaystyle \Стрелка вправо} ∧ {\displaystyle \клин}

Джеймс Бразерстон проделал дальнейшую значительную работу по единой теории доказательств для сгруппированной логики и вариантов, [11] используя понятие логики отображения Белнапа . [12]

Гальмиш, Мери и Пим представили всестороннюю трактовку сгруппированной логики, включая полноту и другие метатеории, основанные на маркированных таблицах . [13]

Приложения

Контроль помех

Возможно, в первом использовании теории субструктурных типов для управления ресурсами Джон К. Рейнольдс показал, как использовать теорию аффинных типов для управления наложением имен и другими формами помех в языках программирования, подобных Алголу . [14] О'Херн использовал теорию сгруппированных типов для расширения системы Рейнольдса, позволяя более гибко смешивать помехи и непомехи. [2] Это решило открытые проблемы, касающиеся рекурсии и скачков в системе Рейнольдса.

Логика разделения

Разделительная логика — это расширение логики Хоара , которое облегчает рассуждения об изменчивых структурах данных, использующих указатели . Согласно логике Хоара, формулы разделительной логики имеют вид , но предусловия и постусловия — это формулы, интерпретируемые в модели сгруппированной логики. Первоначальная версия логики основывалась на следующих моделях: { П г е } п г о г г а м { П о с т } {\displaystyle \{Предварительная\}программа\{Пост\}}

  • ЧАС е а п с = Л ⇀ ф В {\displaystyle Кучи=L\rightharpoonup _{f}V\qquad } (конечные частичные функции от местоположений к значениям)
  • час 0 ∙ час 1 = {\displaystyle h_{0}\bullet h_{1}=} объединение куч с непересекающимися доменами, неопределенное, если домены перекрываются.

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

Логика разделения изначально использовалась для доказательства свойств последовательных программ, но затем была расширена до параллелизма с использованием правила доказательства.

{ П 1 } С 1 { В 1 } { П 2 } С 2 { В 2 } { П 1 ∗ П 2 } С 1 ∥ С 2 { В 1 ∗ В 2 } {\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}} {\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}

который разделяет хранилище, к которому обращаются параллельные потоки. [15]

Позже была использована большая общность семантики ресурсов: абстрактная версия логики разделения работает для троек Хоара, где предусловия и постусловия являются формулами, интерпретируемыми по произвольному частичному коммутативному моноиду вместо конкретной модели кучи. [16] При подходящем выборе коммутативного моноида было неожиданно обнаружено, что правила доказательств абстрактных версий логики параллельного разделения могут использоваться для рассуждений о мешающих параллельных процессах, например, путем кодирования рассуждений на основе rely-gurantee и trace-based. [17] [18]

Логика разделения является основой ряда инструментов для автоматического и полуавтоматического рассуждения о программах и используется в анализаторе программ Infer, который в настоящее время развернут в Facebook. [19]

Ресурсы и процессы

Связанная логика использовалась в сочетании с (синхронным) исчислением ресурсов и процессов SCRP [4] [5] [6] для того, чтобы дать (модальную) логику, которая характеризует, в смысле Хеннесси - Милнера , композиционную структуру параллельных систем.

SCRP примечателен тем, что интерпретируется в терминах как параллельной композиции систем, так и композиции их связанных ресурсов. Семантическое положение логики процесса SCRP, которое соответствует правилу логики разделения для параллелизма, утверждает, что формула истинна в состоянии ресурс-процесс , только в том случае, если есть разложения ресурса и процесса ~ , где ~ обозначает бисимуляцию , такую, что истинна в состоянии ресурс-процесс , и истинна в состоянии ресурс-процесс , ; то есть тогда и только тогда , и . А ∗ Б {\displaystyle А*Б} А ∗ Б {\displaystyle А*Б} Р {\displaystyle R} Э {\displaystyle E} Р = С ∙ Т {\displaystyle R=S\bullet T} Э {\displaystyle E} Ф × Г {\displaystyle F\times G} А {\displaystyle А} С {\displaystyle S} Ф {\displaystyle F} Б {\displaystyle Б} Т {\displaystyle Т} Г {\displaystyle G} Р , Э ⊨ А {\displaystyle R,E\модели A} С , Ф ⊨ А {\displaystyle S,F\models A} T , G ⊨ B {\displaystyle T,G\models B}

Система SCRP [4] [5] [6] основана непосредственно на семантике ресурсов сгруппированной логики; то есть на упорядоченных моноидах элементов ресурсов. Хотя этот выбор и выглядит прямолинейным и интуитивно привлекательным, он приводит к определенной технической проблеме: теорема о полноте Хеннесси–Милнера справедлива только для фрагментов модальной логики, которые исключают мультипликативную импликацию и мультипликативные модальности. Эта проблема решается путем базирования исчисления ресурсного процесса на семантике ресурсов, в которой элементы ресурсов объединяются с использованием двух комбинаторов, один из которых соответствует параллельной композиции, а другой — выбору. [20]

Пространственная логика

Карделли, Кайрес, Гордон и другие исследовали ряд логик исчисления процессов, где конъюнкция интерпретируется в терминах параллельной композиции. [ необходима ссылка ] В отличие от работы Пима и др. в SCRP, они не делают различий между параллельной композицией систем и композицией ресурсов, к которым системы получают доступ.

Их логика основана на примерах семантики ресурсов, которые порождают модели булевой разновидности сгруппированной логики. Хотя эти логики порождают примеры булевой сгруппированной логики, они, по-видимому, были получены независимо и в любом случае имеют значительную дополнительную структуру в виде модальностей и связующих. Связанные логики были также предложены для моделирования XML- данных.

Смотрите также

Ссылки

  1. ^ О'Херн, Питер; Пим, Дэвид (1999). «Логика сгруппированных импликаций» (PDF) . Бюллетень символической логики . 5 (2): 215–244 . CiteSeerX  10.1.1.27.4742 . doi :10.2307/421090. JSTOR  421090. S2CID  2948552.
  2. ^ ab O'Hearn, Peter (2003). "On Bunched Typing" (PDF) . Журнал функционального программирования . 13 (4): 747– 796. doi :10.1017/S0956796802004495.
  3. ^ Иштиак, Самин; О'Херн, Питер (2001). «BI как язык утверждений для изменчивых структур данных» (PDF) . POPL . 28th (3): 14–26 . CiteSeerX 10.1.1.11.4925 . doi :10.1145/373243.375719. 
  4. ^ abc Pym, David; Tofts, Chris (2006). "Исчисление и логика ресурсов и процессов" (PDF) . Формальные аспекты вычислений . 8 (4): 495– 517. doi :10.1007/s00165-006-0018-z. S2CID  16623194.
  5. ^ abc Коллинсон, Мэтью; Пим, Дэвид (2009). «Алгебра и логика для моделирования систем на основе ресурсов». Математические структуры в информатике . 19 (5): 959– 1027. CiteSeerX 10.1.1.153.3899 . doi :10.1017/S0960129509990077. S2CID  14228156. 
  6. ^ abc Коллинсон, Мэтью; Монахан, Брайан; Пим, Дэвид (2012). Дисциплина моделирования математических систем . Лондон: College Publications. ISBN 978-1-904987-50-5.
  7. ^ Пим, Дэвид; О'Херн, Питер; Янг, Хонсок (2004). «Возможные миры и ресурсы: семантика BI». Теоретическая информатика . 315 (1): 257– 305. doi : 10.1016/j.tcs.2003.11.020 .
  8. ^ Дэй, Брайан (1970). «О замкнутых категориях функторов» (PDF) . Отчеты семинара по категориям Среднего Запада IV . Заметки лекций по математике. Т. 137. Springer. С.  1–38 .
  9. ^ Маккаскер, Гай; Пим, Дэвид (2007). "Игровая модель сгруппированных импликаций" (PDF) . Логика компьютерных наук . Конспект лекций по информатике. Том 4646. Springer.
  10. ^ Рид, Стивен (1989). Соответствующая логика: философское исследование вывода . Wiley-Blackwell.
  11. ^ Бразерстон, Джеймс (2012). «Сгруппированные логики, отображаемые» (PDF) . Studia Logica . 100 (6): 1223– 1254. CiteSeerX 10.1.1.174.8777 . doi :10.1007/s11225-012-9449-0. S2CID  13634990. 
  12. ^ Belnap, Nuel (1982). «Логика отображения». Журнал философской логики . 11 (4): 375– 417. doi :10.1007/BF00284976. S2CID  41451176.
  13. ^ Гальмиш, Дидье; Мери, Дэниел; Пим, Дэвид (2005). «Семантика BI и таблиц ресурсов». Математические структуры в информатике . 15 (6): 1033–1088 . CiteSeerX 10.1.1.144.1421 . doi : 10.1017/S0960129505004858 (неактивен с 1 ноября 2024 г.). S2CID  1700033. {{cite journal}}: CS1 maint: DOI inactive as of November 2024 (link)
  14. ^ Рейнольдс, Джон (1978). "Синтаксический контроль помех". Труды 5-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '78 . С.  39–46 . doi : 10.1145/512760.512766 . ISBN 9781450373487. S2CID  18716926.
  15. ^ О'Херн, Питер (2007). "Ресурсы, параллелизм и локальные рассуждения" (PDF) . Теоретическая информатика . 375 ( 1– 3): 271– 307. doi : 10.1016/j.tcs.2006.12.035 .
  16. ^ Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007). "Локальное действие и абстрактная логика разделения" (PDF) . 22-й ежегодный симпозиум IEEE по логике в компьютерных науках (LICS 2007) . стр.  366–378 . CiteSeerX 10.1.1.66.6337 . doi :10.1109/LICS.2007.30. ISBN  978-0-7695-2908-0. S2CID  1044254.
  17. ^ Динсдейл-Янг, Томас; Биркедал, Ларс; Гарднер, Филиппа; Паркинсон, Мэтью; Янг, Хонгсок (2013). «Взгляды: композиционное обоснование для параллельных программ» (PDF) . Труды 40-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . 48 : 287– 300. doi :10.1145/2480359.2429104.
  18. ^ Сергей, Илья; Наневский, Александр; Банерджи, Аниндья (2015). «Определение и проверка параллельных алгоритмов с историями и субъективностью» (PDF) . 24-й Европейский симпозиум по программированию . arXiv : 1410.0306 . Bibcode : 2014arXiv1410.0306S.
  19. ^ Кальканьо, Кристиано; Дистефано, Дино; О'Херн, Питер (11.06.2015). «Открытый исходный код Facebook Infer: выявление ошибок перед отправкой».
  20. ^ Андерсон, Габриэль; Пим, Дэвид (2015). «Исчисление и логика сгруппированных ресурсов и процессов». Теоретическая информатика . 614 : 63–96 . doi : 10.1016/j.tcs.2015.11.035 .
Retrieved from "https://en.wikipedia.org/w/index.php?title=Bunched_logic&oldid=1269337658"