In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theories of some of these structures have then been studied in the presence of additional assumptions, called hypotheses. We propose a unifying framework encompassing all the previous structures, as well as regular tree languages. This is done by considering algebras ordered by complete lattices, where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. Then we study quasi-equational axiomatisations. It is illusory to hope for a generic axiomatisation which would be sound and complete for all instances. Instead, we provide a generic axiomatisation which we prove sound and we setup tools that make it possible to get complete ones in a modular way, building on previous works from the literature. We showcase these tools by proving new completeness results for commutative KA, bi-KA, and regular tree languages, in each case extended with various hypotheses.
翻译:在关于Kleene代数(KA)的文献中,已提出了多种变体,例如带测试的Kleene代数、交换KA、双KA和并发KA。随后,在添加额外假设(称为假设)的情况下,研究了其中一些结构的等式理论。我们提出了一个统一框架,涵盖了所有前述结构以及正则树语言。这是通过考虑由完全格排序的代数来实现的,在该代数中可计算最小不动点。我们提供了一个由闭语言构成的典范模型,并证明其相对于所有连续模型而言是可靠且完备的。随后,我们研究了拟等式公理化。期望存在一种对所有实例均可靠且完备的通用公理化是不切实际的。相反,我们提供了一种经证明可靠的通用公理化,并建立了一系列工具,使其能够基于文献中的先前工作以模块化方式获得完备的公理化。我们通过证明在分别扩展了各种假设的情形下,交换KA、双KA和正则树语言的新的完备性结果,展示了这些工具。