作用代数
在代数逻辑中，作用代数是既是剩余半格又是克莱尼代数的代数结构。它向剩余半格增加了克莱尼代数的星号或自反传递闭包运算，或者说向克莱尼代数增加了剩余半格的左和右剩余或蕴涵运算。不像程序的动态逻辑和其他模态逻辑，对于它们程序和命题形成了两个不同的类别，作用代数合并了二者为一个单一类别。它可被认为是变异的直觉逻辑，带有星号并带有非交换性的合取，它的单位元不需要是顶元素。不像克莱尼代数，作用代数形成了一个簇，它进一步的是可有限公理化的，至关重要的公理是 a·(a → a)* ≤ a。不像克莱尼代数的等式理论的模型(正则表达式等式)，作用代数的星号运算是在所有等式的模型中自反传递闭包。
定义
编辑作用代数 (A, ∨, 0, ·, 1, ←, →, *) 是代数结构使得 (A, ∨, ·, 1, ←, →) 形成剩余半格而 (A, ∨, 0, ·, 1, *) 形成克莱尼代数。就是说，它是接合这两类代数理论的任何模型。现在克莱尼代数是用准等式公理化的，就是说，暗含在两个或更多等式之间，在直接以这种方式公理化的时候作用代数也是如此。使作用代数有特殊价值的是它们有等价的纯粹等式公理化。
在后面我们写不等式 a ≤ b 作为等式 a ∨ b = b 的简写。这允许我们使用不等式公理化理论而在不等式展开为等式的时候仍有纯粹等式公理化。
等式公理化的作用代数是剩余半格，加上下列对于星号的等式。
- 1 ∨ a*·a* ∨ a ≤ a*
- a* ≤ (a∨b)*
- (a → a)* ≤ a → a
第一个等式可分解为三个等式 1 ≤ a*, a*·a* ≤ a* 和 a ≤ a*。它们分别迫使 a* 是自反的、传递的、并大于等于 a。第二个公理断言星号是单调的。第三个公理可以等价的写为 a·(a→a)* ≤ a，这是使它的归纳角色更加明显的形式。着两个公理联合上剩余半格的公理迫使 a* 是大于等于 a 的最小的自反的传递的半格元素。选取其为 a 的自反传递闭包的定义，也就是对于任何作用代数的所有元素 a，a* 是 a 的自反传递闭包。
作用代数的无星号片段的等式理论中，这些不包含星号的等式，可以证明是相符于克莱尼代数的等式理论，也叫做正则表达式等式。在上述公理构成正则表达式的有限公理化的意义上。Redko 在 1967 年证明了这些等式没有有限公理化，约翰·何顿·康威在 1971 年对此给出更短的证明。Salomaa 给出了公理化这个理论的等式模式，Kozen 随后使用准等式或在等式间的蕴涵重新公式化它为有限公理化，至关重要的准等式是归纳的: 如果 x·a ≤ x 则 x·a* ≤ x，和如果 a·x ≤ x 则 a*·x ≤ x。 Kozen 定义克莱尼代数是这种有限公理化的任何模型。
Conway 证明了正则表达式的等式理论允许其中 a* 不是 a 的自反传递闭包的模型，通过给出一个四元素模型 0 ≤ 1 ≤ a ≤ a* 其中 a·a = a。在 Conway 的模型中，a 是自反和传递的，因此它的自反传递闭包应该是 a。但是正则表达式不确保如此，它允许 a* 严格大于 a。这种反常行为在作用代数中是不可能的。
例子
编辑任何Heyting代数(因此任何布尔代数)通过选取 · 为 ∧ 和 a* = 1 就得到了一个作用代数。这对于星号是必要和充分的，因为 Heyting 代数的顶元素 1 是它的唯一自反元素，并且是传递的，还大于等于这个代数的所有元素。
在字母表 Σ 上所有形式语言(有限字符串的集合)的集合 2Σ* 形成了一个作用代数，带有 0 为空集，1 = {ε}，∨ 为并集，· 为串接，L←M 为所有字符串 x 使得 xM ⊆ L 的集合(对偶于 M→L)，而 L* 是在 L 中字符串形成的所有字符串的集合(Kleene闭包)。
在集合 X 上的所有二元关系的集合 形成一个作用代数，带有 0 为空关系，1 为恒等关系或等式，∨ 为并集，· 为关系复合，R←S 为所有有序对 (x,y) 使得对于所有 X 中的 z 有 ySz 蕴涵 xRz 所构成的关系(对偶于 S→R)，和 R* 为 R 的自反传递闭包，定义为在所有关系 Rn 对整数 n ≥ 0 的并集。
参见
编辑引用
编辑- J.H. Conway, Regular Algebra and Finite Machines, Chapman and Hall, London, 1971.
- D. Kozen, On Kleene algebras and closed semirings, In B. Rovan, editor, Mathematical Foundations of Computer Science 1990, LNCS 452, 26--47, Banska Bystrica, Springer-Verlag, 1990.
- V.R. Pratt, Action Logic and Pure Induction, Logics in AI: European Workshop JELIA '90 (ed. J. van Eijck), LNCS 478, 97--120, Springer-Verlag, 1990.
- V.N. Redko, On defining relations for the algebra of regular events (Russian), Ukrain. Mat. Z., 16:120--126, 1964.