论文标题
关于与假设的Kleene代数完整的工具
On Tools for Completeness of Kleene Algebra with Hypotheses
论文作者
论文摘要
在有关Kleene代数的文献中，已经提出了许多变体，这些变体施加了由理论指定的其他结构，例如具有测试（KAT）的Kleene代数（KAT）和最近具有观察结果的Kleene代数（KAO），或者对某些某些常数进行特定的假设，例如在NetKat中。这些变体中的许多都符合克莱恩代数提供的假设提供的统一观点，该观点带有一个规范的语言模型，该模型由给定的一组假设构建。对于KAT，该模型对应于将表达式作为守卫字符串语言的熟悉解释。因此，一个相关的问题是，Kleene代数以及给定的一组假设是否相对于其规范语言模型完成。在本文中，我们在此问题上重新审视，结合和扩展现有结果，以获取以模块化方式证明完整性的工具。我们通过为Kat，Kao和Netkat提供新的和模块化的完整性证明来展示这些工具，我们证明了Kat：Kat的新变体的完整性，以全面关系扩展，kat进行了逆操作，并以逆向操作扩展了KAT，而KAT的版本则是测试的收集，仅形成了分布式效果。
In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.
