Сгруппированная логика

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

Фонды [ править ]

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

${\ Displaystyle A \ клин B \ vdash C \ quad {\ mbox {iff}} \ quad A \ vdash B \ Rightarrow C}$

Сгруппированная логика имеет две версии теоремы дедукции:

${\ Displaystyle A * B \ vdash C \ quad {\ mbox {iff}} \ quad A \ vdash B {- \! \! *} C \ qquad {\ mbox {, а также}} \ qquad A \ клин B \ vdash C \ quad {\ mbox {iff}} \ quad A \ vdash B \ Rightarrow C}$

${\ displaystyle A * B}$и являются формами соединения и импликации, которые принимают во внимание ресурсы (поясняется ниже). В дополнение к этим связкам в сгруппированной логике есть формула, иногда обозначаемая буквой I или emp, которая является единицей измерения *. В исходной версии сгруппированной логики и были связки интуиционистской логики, тогда как логический вариант берет and (и ) как из традиционной булевой логики. Таким образом, сгруппированная логика совместима с конструктивными принципами, но никоим образом от них не зависит.${\ displaystyle B {- \! \! *} C}$${\ Displaystyle \ клин}$${\ displaystyle \ Rightarrow}$${\ Displaystyle \ клин}$${\ displaystyle \ Rightarrow}$${\ displaystyle \ neg}$

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

Самый простой способ понять эти формулы - с точки зрения их функциональной семантики истинности. В этой семантике формула истинна или ложна по отношению к данным ресурсам. утверждает, что данный ресурс можно разложить на ресурсы, удовлетворяющие требованиям и . говорит, что если мы объединяем имеющийся ресурс с дополнительным ресурсом, который удовлетворяет , то объединенный ресурс удовлетворяет . и имеют знакомые значения.${\ displaystyle A * B}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle B {- \! \! *} C}$${\ displaystyle B}$${\ displaystyle C}$${\ Displaystyle \ клин}$${\ displaystyle \ Rightarrow}$

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

${\displaystyle r\models A*B\quad {\mbox{iff}}\quad \exists r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{and}}\,r_{A}\bullet r_{B}\leq r}$

где - способ объединения ресурсов, а - отношение приближения.${\displaystyle r_{A}\bullet r_{B}}$${\displaystyle \leq }$

Эта семантика сгруппированной логики опирается на предыдущую работу в Relevant Logic (особенно на операционную семантику Рутли-Мейера), но отличается от нее тем, что не требует и принимает семантику стандартных интуиционистских или классических версий и . Свойство оправдано, когда думают о релевантности, но отрицается соображениями ресурса; наличие двух копий ресурса - это не то же самое, что наличие одной, и в некоторых моделях (например, моделях кучи) может даже не быть определено. Стандартная семантика ${\displaystyle r\bullet r\leq r}$${\displaystyle \wedge }$${\displaystyle \Rightarrow }$${\displaystyle r\bullet r\leq r}$${\displaystyle r\bullet r}$${\displaystyle \Rightarrow }$(или отрицания) часто отвергаются релевантистами в их попытках избежать «парадоксов материального подтекста», которые не являются проблемой с точки зрения моделирования ресурсов и, следовательно, не отвергаются сгруппированной логикой. Семантика также относятся к «фазе семантике» линейной логики, но опять - таки отличается от принятия стандарта (даже булева) семантики и что в линейной логике отвергаются в попытке быть конструктивными. Эти соображения подробно обсуждаются в статье Пима, О'Хирна и Янга о семантике ресурсов. ^[7]${\displaystyle \wedge }$${\displaystyle \Rightarrow }$

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

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

${\displaystyle Hom(A\wedge B,C)\quad {\mbox{is isomorphic to}}\quad Hom(A,B\Rightarrow C)}$

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

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

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

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

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

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

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

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

Теория доказательств и теория типов (пучки) [ править ]

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

${\displaystyle {\frac {\Gamma ,A\vdash B}{\Gamma \vdash A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;A\vdash B}{\Gamma \vdash A{\Rightarrow }B}}}$

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

• Мультипликативная композиция отрицает структурные правила ослабления и сжатия.${\displaystyle \Delta ,\Gamma }$
• Аддитивный состав допускает ослабление и сжатие целых пучков.${\displaystyle \Delta ;\Gamma }$

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

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

${\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x.M:A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;x:A\vdash M:B}{\Gamma \vdash \alpha x.M:A{\Rightarrow }B}}}$

Здесь есть два разных связывателя и по одному для каждого типа функции.${\displaystyle \lambda }$${\displaystyle \alpha }$

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

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

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

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

Контроль помех [ править ]

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

Логика разделения [ править ]

Логика разделения - это расширение логики Хоара, которое упрощает рассуждения об изменяемых структурах данных, использующих указатели. Следуя логике Хоара, формулы логики разделения имеют форму , но предусловия и постусловия являются формулами, интерпретируемыми в модели сгруппированной логики. Исходная версия логики была основана на следующих моделях:${\displaystyle \{Pre\}program\{Post\}}$

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

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

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

${\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] Путем подходящего выбора коммутативного моноида было неожиданно обнаружено, что правила доказательства абстрактных версий логики параллельного разделения могут использоваться для рассуждений о вмешательстве в параллельные процессы, например, путем кодирования основанных на гарантии и трассировок рассуждений. ^{[17] [18]}

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

Ресурсы и процессы [ править ]

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

SCRP примечателен интерпретации с точки зрения как параллельной композиции систем и состава связанных с ними ресурсов. Семантическое предложение логики процесса SCRP, которое соответствует правилу логики разделения для параллелизма, утверждает, что формула верна в состоянии ресурс-процесс , на всякий случай, когда есть декомпозиции ресурса и процесса ~ , где ~ обозначает бимоделирование, такое, что истинно в состояние ресурсов процесс , и это верно в состоянии ресурсов процесса , ; то есть тогда и только тогда .${\displaystyle A*B}$${\displaystyle A*B}$${\displaystyle R}$${\displaystyle E}$${\displaystyle R=S\bullet T}$${\displaystyle E}$${\displaystyle F\times G}$${\displaystyle A}$${\displaystyle S}$${\displaystyle F}$${\displaystyle B}$${\displaystyle T}$${\displaystyle G}$${\displaystyle R,E\models A}$${\displaystyle S,F\models A}$${\displaystyle T,G\models B}$

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

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

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

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

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

• Логика разделения
• Логика релевантности
• Линейная логика

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