在代数逻辑中，作用代数是既是剩余半格又是克莱尼代数的代数结构。它向剩余半格增加了克莱尼代数的星号或自反传递闭包运算，或者说向克莱尼代数增加了剩余半格的左和右剩余或蕴涵运算。

作用代数的概念(概念简述 定义)

等式公理化(有星号的等式理论 无星号片段的等式理论)

相关概念(Kleene 星号 正则表达式)

例子

作用代数的概念

概念简述

不像程序的动态逻辑和其他模态逻辑，对于它们程序和命题形成了两个不同的类别，作用代数合并了二者为一个单一类别。它可被认为是变异的直觉逻辑，带有星号并带有非交换性的合取，它的单位元不需要是顶元素。不像克莱尼代数，作用代数形成了一个簇，它进一步的是可有限公理化的，至关重要的公理是 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。这种反常行为在作用代数中是不可能的。

相关概念

Kleene 星号

Kleene 星号，或称 Kleene 闭包，德语称 Kleensche Hülle，在数学上是一种适用于字符串或符号及字符的集合的一元运算。当 Kleene 星号被应用在一个集合V时，写法是V*。它被广泛用于正则表达式。

如果 V是 M的子集，则 V* 被定义为包含 ε(空字符串)并闭合于这个运算下的 V的最小超集。接着 V* 自身是幺半群，并被称为“V 生成的自由幺半群”。这是上面讨论的 Kleene 星号的推广，因为在某个符号的集合上所有字符串的集合形成了一个幺半群(带有字符串串接作为二元运算)。

正则表达式

1. 概述

（英语：Regular Expression、regex或regexp，缩写为RE），也译为正规表示法、常规表示法，在计算机科学中，是指一个用来描述或者匹配一系列符合某个句法规则的字符串的单个字符串。在很多文本编辑器或其他工具里，正则表达式通常被用来检索和/或替换那些符合某个模式的文本内容。许多程序设计语言都支持利用正则表达式进行字符串操作。例如，在Perl中就内建了一个功能强大的正则表达式引擎。正则表达式这个概念最初是由Unix中的工具软件（例如sed和grep）普及开的。正则表达式通常缩写成“regex”，单数有regexp、regex，复数有regexps、regexes、regexen。

2. 基本概念

一个正则表达式通常被称为一个模式 (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”是相同的。

精确的语法可能因不同的工具或程序而异。

3. 形式化语言理论

正则表达式可以用形式化语言理论的方式来表达。正则表达式由常量和算子组成，它们分别指示字符串的集合和在这些集合上的运算。给定有限字母表 Σ 定义了下列常量:

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

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

(“文字字符”) 在 Σ 中的 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*。

例子

任何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 的并集。