作用代數

不像程序的動態邏輯和其他模態邏輯，對於它們程序和命題形成了兩個不同的類別，作用代數合併了二者為一個單一類別。它可被認為是變異的直覺邏輯，帶有星號並帶有非交換性的合取，它的單位元不需要是頂元素。不像克萊尼代數，作用代數形成了一個簇，它進一步的是可有限公理化的，至關重要的公理是 a·(a→ a)* ≤ a。不像克萊尼代數的等式理論的模型(正則表達式等式)，作用代數的星號運算是在所有等式的模型中自反傳遞閉包。

作用代數 (A, ∨, 0, ·, 1, ←, →, *) 是代數結構使得 (A, ∨, ·, 1, ←, →) 形成剩餘半格而 (A, ∨, 0, ·, 1, *) 形成克萊尼代數。就是説，它是接合這兩類代數理論的任何模型。克萊尼代數是用準等式公理化的，就是説，暗含在兩個或更多等式之間，在直接以這種方式公理化的時候作用代數也是如此。使作用代數有特殊價值的是它們有等價的純粹等式公理化。

在後面我們寫不等式 a≤ b作為等式 a∨ b= b的簡寫。這允許我們使用不等式公理化理論而在不等式展開為等式的時候仍有純粹等式公理化。 ^[1] 

等式公理化的作用代數是剩餘半格，加上下列對於星號的等式。

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。這種反常行為在作用代數中是不可能的。 ^[1] 

Kleene 星號，或稱 Kleene 閉包，德語稱 Kleensche Hülle，在數學上是一種適用於字符串或符號及字符的集合的一元運算。當 Kleene 星號被應用在一個集合V時，寫法是V*。它被廣泛用於正則表達式。

如果 V是 M的子集，則 V* 被定義為包含 ε(空字符串)並閉合於這個運算下的 V的最小超集。接着 V* 自身是幺半羣，並被稱為“V 生成的自由幺半羣”。這是上面討論的 Kleene 星號的推廣，因為在某個符號的集合上所有字符串的集合形成了一個幺半羣(帶有字符串串接作為二元運算)。

（英語：Regular Expression、regex或regexp，縮寫為RE），也譯為正規表示法、常規表示法，在計算機科學中，是指一個用來描述或者匹配一系列符合某個句法規則的字符串的單個字符串。在很多文本編輯器或其他工具裏，正則表達式通常被用來檢索和/或替換那些符合某個模式的文本內容。許多程序設計語言都支持利用正則表達式進行字符串操作。例如，在Perl中就內建了一個功能強大的正則表達式引擎。正則表達式這個概念最初是由Unix中的工具軟件（例如sed和grep）普及開的。正則表達式通常縮寫成“regex”，單數有regexp、regex，複數有regexps、regexes、regexen。

一個正則表達式通常被稱為一個模式 (pattern)，為用來描述或者匹配一系列符合某個句法規則的字符串。例如：Handel、Händel和 Haendel這三個字符串，都可以由“H(a|ä|ae)ndel”這個模式來描述。大部分正則表達式的形式都有如下的結構：

選擇|豎直分隔符代表選擇。例如“gray|grey”可以匹配grey或gray。數量限定某個字符後的數量限定符用來限定前面這個字符允許出現的個數。最常見的數量限定符包括“+”、“?”和“*”（不加數量限定則代表出現一次且僅出現一次）：+加號代表前面的字符必須至少出現一次。(1次、或多次)。例如，“goo+gle”可以匹配google、gooogle、goooogle等;?問號代表前面的字符最多隻可以出現一次。(0次、或1次)。例如，“colou?r”可以匹配color或者colour;*星號代表前面的字符可以不出現，也可以出現一次或者多次。(0次、或1次、或多次)。例如，“0*42”可以匹配42、042、0042、00042等。匹配圓括號可以用來定義操作符的範圍和優先度。例如，“gr(a|e)y”等價於“gray|grey”，“(grand)?father”匹配father和grandfather。

上述這些構造子都可以自由組合，因此，“H(ae?|ä)ndel”和“H(a|ae|ä)ndel”是相同的。

精確的語法可能因不同的工具或程序而異。

正則表達式可以用形式化語言理論的方式來表達。正則表達式由常量和算子組成，它們分別指示字符串的集合和在這些集合上的運算。給定有限字母表 Σ 定義了下列常量:

(“空集”) ∅指示集合 ∅

(“空串”) ε 指示集合 {ε}

(“文字字符”) 在 Σ 中的 a指示集合 {a}

定義了下列運算:

(“串接”) RS指示集合 { αβ | α ∈ R∧ β ∈ S}。例如 {"ab"|"c"}{"d"|"ef"} = {"abd", "abef", "cd", "cef"}。

(“選擇”) R|S指示 R和 S的並集。

(“Kleene星號”) R* 指示包含 ε 並且閉包在字符串串接下的 R的最小超集。這是可以通過 R中的零或多個字符串的串接得到所有字符串的集合。例如，{"ab", "c"}* = {ε, "ab", "c", "abab", "abc", "cab", "cc", "ababab", ... }。

上述常量和算子形成了克萊尼代數。

很多課本使用對選擇使用符號 ∪, +或 ∨替代豎槓。

為了避免括號，假定 Kleene 星號有最高優先級，接着是串接，接着是並集。如果沒有歧義則可以省略括號。例如，(ab)c可以寫為 abc而 a|(b(c*))可以寫為 a|bc*。 ^[2] 

任何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的自反傳遞閉包，定義為在所有關係 R對整數 n≥ 0 的並集。 ^[1]