KAT方程组到KA方程组的易化
Feasibly Reducing KAT Equations to KA Equations
摘要：
Kleene代数（KA）是正则事件的代数。Kleene代数的常见例子包括正则集、关系代数和迹代数。带有测试的Kleene代数（KAT）是一个带有嵌入布尔子代数的Kleene代数。测试的增加允许将{ \tt while}程序编码为KAT项，因此KAT的等式理论可以表示（命题）程序等价。关于程序的更复杂的陈述可以用KAT的霍尔理论来表达，它足以编码命题霍尔逻辑。科恩等人已经证明，KAT的方程理论简化为KA的方程理论。不幸的是，他们的简化涉及到所涉及的项的大小的指数爆炸。在这里，我们给出一个替代的可行约简。
英文摘要：
Kleene algebra (KA) is the algebra of regular events. Familiar examples of Kleene algebras include regular sets, relational algebras, and trace algebras. A Kleene algebra with tests (KAT) is a Kleene algebra with an embedded Boolean subalgebra. The addition of tests allows one to encode {\tt while} programs as KAT terms, thus the equational theory of KAT can express (propositional) program equivalence. More complicated statements about programs can be expressed in the Hoare theory of KAT, which suffices to encode Propositional Hoare Logic. That the equational theory of KAT reduces to the equational theory of KA has been shown by Cohen et al. Unfortunately, their reduction involves an exponential blowup in the size of the terms involved. Here we give an alternate feasible reduction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
