论文标题
一级程序代数
One-sorted Program Algebras
论文作者
论文摘要
KAT KAT KLEENE代数提供了一个简单的两排代数框架，用于验证程序时命题的属性。 Kleene代数与域，KAD是Kat的单排替代方案。 Kat的方程理论嵌入KAD中，但Kad缺乏KAT的一些自然特性。例如，并非每个Kleene代数都会扩展到KAD，并且每个KAD中的测试子代数被迫是负锥的最大布尔子代数。在本文中，我们提出了KAD的概括，该KAD避免了这些特征，同时仍嵌入KAT的方程理论。我们表明，可以将KAD域操作员的几种自然特性添加到广义框架中，而不会影响结果。我们考虑了框架的变体，其中使用Kleene代数乘法的残差定义了测试互补。
Kleene algebra with tests, KAT, provides a simple two-sorted algebraic framework for verifying properties of propositional while programs. Kleene algebra with domain, KAD, is a one-sorted alternative to KAT. The equational theory of KAT embeds into KAD, but KAD lacks some natural properties of KAT. For instance, not each Kleene algebra expands to a KAD, and the subalgebra of tests in each KAD is forced to be the maximal Boolean subalgebra of the negative cone. In this paper we propose a generalization of KAD that avoids these features while still embedding the equational theory of KAT. We show that several natural properties of the domain operator of KAD can be added to the generalized framework without affecting the results. We consider a variant of the framework where test complementation is defined using a residual of the Kleene algebra multiplication.
