集束蕴涵与分离逻辑的代数一瞥
An Algebraic Glimpse at Bunched Implications and Separation Logic
摘要：
我们从小野宏明的代数方法的启发，子结构逻辑的角度概述了集束蕴涵（BI）和分离逻辑（SL）的逻辑。我们提出广义BI代数（GBI代数）作为一个共同的框架，代数产生通过“声明性资源阅读”，直觉主义的关系代数和箭头逻辑和分配Lambek演算的直觉主义的含义。除了现有的BI模型（特别是堆模型和效果代数），我们还涵盖了模型所产生的弱化关系，形式语言或更细粒度的治疗标记树和半结构化数据。在简要讨论了GBI的子簇格之后，我们沿着Esakia和Priestley的思路给出了GBI的一个合适的对偶，并在Galatos和Jipsen的剩余标架的背景下给出了割消的代数证明.我们还展示了如何代数方法允许通用的结果的可判定性，积极和消极的。在本文的最后一部分，我们轻轻地介绍了一些理论背后的最先进的工具，最终与代数和证明理论介绍（双）溯因。
英文摘要：
We overview the logic of Bunched Implications (BI) and Separation Logic (SL) from a perspective inspired by Hiroakira Ono's algebraic approach to substructural logics. We propose generalized BI algebras (GBI-algebras) as a common framework for algebras arising via "declarative resource reading", intuitionistic generalizations of relation algebras and arrow logics and the distributive Lambek calculus with intuitionistic implication. Apart from existing models of BI (in particular, heap models and effect algebras), we also cover models arising from weakening relations, formal languages or more fine-grained treatment of labelled trees and semistructured data. After briefly discussing the lattice of subvarieties of GBI, we present a suitable duality for GBI along the lines of Esakia and Priestley and an algebraic proof of cut elimination in the setting of residuated frames of Galatos and Jipsen. We also show how the algebraic approach allows generic results on decidability, both positive and negative ones. In the final part of the paper, we gently introduce the substructural audience to some theory behind state-of-art tools, culminating with an algebraic and proof-theoretic presentation of (bi-)abduction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
