论文标题
树木共享结构的复杂性分析
Complexity Analysis of Tree Share Structure
论文作者
论文摘要
Dockins等人提出的树木共享结构。是一个优雅的模型，用于跟踪并发分离逻辑中的不交互所有权，但是由于缺乏系统的理论研究，因此很难实施树木份额的决策程序。我们表明，整个布尔代数的一阶理论（即带有所有树状常数）是可决定的，并且具有与可数原子布尔代数的一阶理论相同的复杂性。我们证明，将此加性结构与恒定限制的单一乘法“相对化”运算符相结合，具有非元素下限。我们研究了这种下限的后果，并证明了它是通过证明隔离限制乘法理论的上限来证明这两种理论的组合。
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (that is, with all tree-share constants) is decidable and has the same complexity as of the first-order theory of Countable Atomless Boolean Algebras. We prove that combining this additive structure with a constant-restricted unary multiplicative "relativization" operator has a non-elementary lower bound. We examine the consequences of this lower bound and prove that it comes from the combination of both theories by proving an upper bound on a generalization of the restricted multiplicative theory in isolation.
