作用代數
在代數邏輯中，作用代數是既是剩餘半格又是克萊尼代數的代數結構。它向剩餘半格增加了克萊尼代數的星號或自反傳遞閉包運算，或者說向克萊尼代數增加了剩餘半格的左和右剩餘或蘊涵運算。不像程序的動態邏輯和其他模態邏輯，對於它們程序和命題形成了兩個不同的類別，作用代數合併了二者為一個單一類別。它可被認為是變異的直覺邏輯，帶有星號並帶有非交換性的合取，它的單位元不需要是頂元素。不像克萊尼代數，作用代數形成了一個簇，它進一步的是可有限公理化的，至關重要的公理是 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.