Введение

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

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

Алгебраическая семантика групповой логики является частным случаем ее категориальной семантики, но ее проще сформулировать, и она может быть более понятной. Алгебраическая модель групповой логики – это частично упорядоченное множество, являющееся алгеброй Гейтинга и несущее дополнительную структуру коммутативной решетки с остатком (для той же решетки, что и алгебра Гейтинга): то есть упорядоченный коммутативный моноид с ассоциированной импликацией, удовлетворяющей определенным условиям. Булева версия групповой логики имеет следующие модели. Алгебраическая модель булевой групповой логики – это частично упорядоченное множество, являющееся булевой алгеброй и несущее дополнительную структуру коммутативного моноида с остатком.

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

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