Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to behaviors of GKAT expressions. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.
翻译:保护 Kleene 代数与测试( GKAT) 是 KAT 的有效碎片, 因为它允许几乎线性变异。 在本文中, 我们研究了 GKAT 的( co) 代数特性 。 我们最初的焦点是通过省略所谓的早期终止轴来区分执行不同动作的不成功程序的碎片 。 我们开发了一个操作( coalgebraic) 和 代数( algebraic) 语义, 并显示它们同时存在 。 然后我们描述 GKAT 表达方式在这个语义中的行为, 从而形成一种对比, 捕捉到与 GKAT 表达方式的行为相对应的自动成形的共性 。 最后, 我们证明, 减小的碎片的正数是声音和完整的 w.r. t. 语义, 然后以此结果为基础, 恢复出一个声音和完整的 w.r. t. 方形的语义 。