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

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

Фонды

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

$A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C$

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

$A*B\vdash C\quad {\mbox{iff}}\quad A\vdash B{-\!\!*}C\qquad {\mbox{and also}}\qquad A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C$

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

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

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

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

$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$

где $r_{A}\bullet r_{B}$ это способ объединения ресурсов и $\leq$ является отношением аппроксимации.

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

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

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

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

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

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

Дэя, можно создать множество категориальных моделей . тензорного произведения Используя конструкцию Дополнительно импликативному фрагменту группированной логики придана игровая семантика .

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

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

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

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

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

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

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

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

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

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

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

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

${\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}}$

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

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

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

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

Приложения

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

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

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

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

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

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

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

${\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}\}}}$

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

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

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

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

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

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

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

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

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

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

См. также

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