带有测试的幺半群和可能非停机程序的代数
Monoids with tests and the algebra of possibly non-halting programs
摘要：
我们研究可计算函数的代数理论，它可以被看作是从可能的非停机计算机程序或算法中产生的，作用于某些状态空间，配备了组合运算，{ \em if-then-else}和{ \em while-do}根据条件的布尔代数定义。以前已经证明，在这些操作下，部分函数的代数没有有限的公理化，即使人们将注意力限制在变换（表示停机程序）而不是部分函数上，并且从签名中省略{ \em while-do}，这也是成立的。在停机的情况下，有一个自然的“修复”，这是允许组合停机程序的条件，然后得到的代数承认有限的公理化。在目前的设置这样的组合是不可能的，但通过扩展的概念{ \em if-then-else}，我们能够给有限公理化的结果代数（部分）功能，与{ \em while-do}的签名，如果状态空间是假定有限的。公理化扩展到考虑部分谓词的平等。所有的代数被认为是丰富的概念（单侧）限制半群。
英文摘要：
We study the algebraic theory of computable functions, which can be viewed as arising from possibly non-halting computer programs or algorithms, acting on some state space, equipped with operations of composition, {\em if-then-else} and {\em while-do} defined in terms of a Boolean algebra of conditions. It has previously been shown that there is no finite axiomatisation of algebras of partial functions under these operations alone, and this holds even if one restricts attention to transformations (representing halting programs) rather than partial functions, and omits {\em while-do} from the signature. In the halting case, there is a natural "fix", which is to allow composition of halting programs with conditions, and then the resulting algebras admit a finite axiomatisation. In the current setting such compositions are not possible, but by extending the notion of {\em if-then-else}, we are able to give finite axiomatisations of the resulting algebras of (partial) functions, with {\em while-do} in the signature if the state space is assumed finite. The axiomatisations are extended to consider the partial predicate of equality. All algebras considered turn out to be enrichments of the notion of a (one-sided) restriction semigroup.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
