具有传递交换性条件的克林代数
Kleene Algebra with Transitive Commutativity Conditions
浏览论文内容
中文总结 AI 辅助
研究克林代数KA在添加交换性条件C后的等式理论可判定性问题，证明其可判定当且仅当C是传递的，还从正反两方面强化结果，即C非传递时普遍性问题不可判定，传递时KA* + C和KA + C等式理论一致。
中文摘要 AI 辅助
克林代数（KA）为推理程序结构和控制流提供了基础代数框架。为捕捉动作重新排序或独立产生的等价关系，Kozen提议用交换性条件扩展KA。本文研究问题：对于哪些关系C，KA + C的等式理论是可判定的？早期相关工作表明正则语言模交换性条件C可判定当且仅当C是传递的。对于克林代数KA和交换性条件C，情况更困难。Kuznetsov最近表明在某些特定交换性条件下克林代数KA + C的等式理论不可判定。本文完全解决此问题，证明KA + C的等式理论可判定当且仅当C是传递的。此外，从正反两方面强化了结果。负面表明当C非传递时，KA + C的普遍性问题已不可判定；正面表明对于传递的C，KA* + C和KA + C的等式理论一致。
英文摘要
Kleene algebra (KA) provides a foundational algebraic framework for reasoning about program structure and control flow. To capture equivalences arising from reordering or independence of actions, Kozen [1996] purposed that KA can be extended with commutativity conditions, that is, equations of the form { ab = ba | (a,b) \in C }, where C is a binary relation on constant symbols. This paper studies the following question: for which relations C is the equational theory of KA+C decidable? Early related work [Bertoni et al. 1982; Ibarra 1978] showed that regular languages modulo commutativity conditions C are decidable if and only if C is transitive. For Kleene algebra KA and commutativity conditions C, however, the situation is substantially more difficult. Only very recently, Kuznetsov [2023] showed that the equational theory of Kleene algebra KA+C is undecidable under certain specific commutativity conditions, settling the first nontrivial cases more than 25 years after the corresponding problem for KA* +C was resolved by Kozen [1996]. Nevertheless, the decidability problem of KA+C remained open. In this work, we resolve this question completely by showing that the equational theory of KA+C is decidable if and only if C is transitive. Moreover, we strengthen the result in both directions. On the negative side, we show that when C is not transitive, the universality problem for KA+C is already undecidable. On the positive side, we show that for transitive C, the equational theories of KA* +C and KA+C coincide.
