具有恶魔精化的半群之有限可表示性

二元关系的复合与恶魔精化 $\sqsubseteq$ 定义为 \begin{align*} (x, y)\in (R;S)&\iff \exists z((x, z)\in R\wedge (z, y)\in S) R\sqsubseteq S&\iff (dom(S)\subseteq dom(R) \wedge R\restriction_{dom(S)}\subseteq S) \end{align*} 其中 $dom(S)=\{x:\exists y (x, y)\in S\}$ 且 $R\restriction_{dom(S)}$ 表示 $R$ 限制于满足 $x\in dom(S)$ 的对 $(x, y)$。恶魔演算被引入以建模非确定性程序的全正确性，并已应用于程序验证。我们证明，同构于一组按恶魔精化排序且带复合的二元关系的抽象 $(\leq, \circ)$ 结构类 $R(\sqsubseteq, ;)$ 无法由任何有限集的一阶 $(\leq, \circ)$ 公式公理化。我们给出了一个相当简单、无穷的递归公理化来定义 $R(\sqsubseteq, ;)$。我们证明有限可表示 $(\leq, \circ)$ 结构在有限基上具有表示。这似乎是首个带复合的二元关系签名中，表示类不可有限公理化但有限可表示结构具有有限表示性质的例子。