单排序程序代数
One-sorted Program Algebras
摘要：
Kleene代数与测试，KAT，提供了一个简单的两个排序的代数框架，验证性质的命题，而程序。带Domain的Kleene代数KAD是KAT的一种单排序替代。KAT的方程理论嵌入到KAD中，但KAD缺乏KAT的一些自然属性。例如，不是每个Kleene代数都能扩展成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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
