有限迹属性并发系统的无切分 Sequent Calculus

我们致力于识别一个能够用于分析并发系统中有限迹属性的证明论框架，尤其关注由前缀闭合指定的属性。为此，我们研究了前缀闭合算子及其剩余运算（相对于集合包含关系）与语言交叉、并、串的相互作用，提出了闭合$\ell$-幺半群的概念作为有限迹属性的最小代数抽象，以便在分析性证明系统中便利地描述。闭合$\ell$-幺半群是分配式剩余 lattice 的无除法还原，配备一个前向菱形/后向盒残留的单元一模态算子对，其中菱形是满足$\Diamond(x \cdot y) \leq \Diamond x \cdot \Diamond y$的拓扑闭合算子。作为这些结构的逻辑对应物，我们呈现$\mathsf{LMC}$，这是一种基于分配式完全Lambek Calculus无除法片段的Gentzen式系统。在$\mathsf{LMC}$中，结构项是使用Belnap式结构运算符从公式构建的，用于幺半群乘法、meet和菱形。模态和结构菱形的规则取自Moortgat的系统$\mathsf{NL}(\Diamond)$。我们证明该计算是sound且complete的，适用于闭合$\ell$-幺半群的 variety，并且它允许cut消除。