Skip to content

Kleene 定理

Kleene's theorem

经典正则表达式描述的有限字语言恰好是有限自动机能够识别的语言。

条目类型
定理

形式陈述

对任意 LΣ,以下条件等价:

  1. L=L(R),其中 R 是经典正则表达式
  2. L 可由某台ε-NFA 或 NFA 识别;
  3. L 可由某台 DFA 识别。

从表达式到 ε-NFA 的方向按语法结构归纳。ε 和单符号 a 各有常数大小的基本自动机;若已经为 R,S 构造机器,就用 ε-边接线实现并、连接和星。每个模板都保持“从组件入口到出口的路径标签恰是相应语言”这一不变量,因此归纳得到 L(NR)=L(R)。再应用DFA–NFA 等价定理,便得到等价 DFA。

反方向可用广义 NFA 的状态消除证明。广义 NFA 的一条边允许标记正则表达式,路径通过连接边语言、并合备选路径来解释。消去中间状态 k 时,把每对保留状态 i,j 的边标签更新为

RijRik(Rkk)Rkj.

第一项保留所有不经过 k 的路径;第二项描述先到 k、在 k 处循环任意次、再离开 k 的路径。更新后,任意两保留状态之间可由内部已消除状态经过的路径语言不变。最终只剩新初态和新接受态,其边标签就是原自动机语言的正则表达式。

同一论证也可写成动态规划。令 Rij(k) 描述从 ij 且内部节点只取前 k 个状态的路径标签,则

Rij(k)=Rij(k1)Rik(k1)(Rkk(k1))Rkj(k1).

这个递推正好按“是否经过状态 k”划分所有路径,是状态消除正确性的证明骨架,而不只是一个符号操作口诀。

直觉

正则表达式和自动机从相反方向描述同一件事。表达式把合法字拆成选择、顺序与重复;自动机把已读前缀压缩成有限状态并沿输入推进。Thompson 构造把语法树摊成控制流图,状态消除则把图中所有可能路径重新折叠成一个代数式。

ε-边是两种世界之间的接缝。表达式的并需要在两个组件入口间选择,连接需要从前一组件出口跳到后一入口,星需要允许零次进入和反复返回;这些选择都不应消耗输入,所以 ε-NFA 让结构归纳保持局部。确定化是在翻译完成后把所有候选控制位置合成集合状态。

等价是外延的:两种表示定义同一个字集合。它不保存语法树、匹配捕获、路径数量或运行方式,也不保证长度相近。一个紧凑 NFA 可能确定化为指数多状态,自动机消除状态后也可能得到巨大且难读的表达式。

Kleene 定理示意图
例子与边界

表达式

(ifin)

按字符字母表展开后,两条分支共享首字符 i。Thompson 构造可以先为两个词分别建路径,再用 ε-边从新初态选择分支;后续 NFA 化简或确定化会把公共前缀合并。构造首先追求结构正确,是否共享状态属于独立的表示优化。

反向看,一台追踪 1 个数奇偶性的两状态 DFA 可被消除成正则表达式。表达式形式会随消除顺序改变,例如可以把任意数量的 0 穿插在成对的 1 之间;这些外观不同的结果只要描述同一语言就都正确。状态消除不是求某个唯一“标准表达式”。

定理的边界由“经典”二字规定。带反向引用的引擎模式可能要求后半段复现任意长的捕获文本,已不再是有限状态性质;另一方面,字符类、有限重复 {m,n} 和懒惰量词若不改变接受集合,通常只是经典表达式的语法糖或匹配策略。判断能力时应看精确定义,而不是工具名称。

Kleene 定理也不涵盖无限字。Büchi 自动机与 ω-正则表达式有相应理论,但接受条件与星/无限迭代的语义不同,不能把有限字状态消除直接当作证明。

推论与应用

定理让正则语言成为与表示无关的类别。需要人类编写时选表达式,需要局部组合时选 ε-NFA,需要稳定执行、取补或最小化时选 DFA;每一步都可证明保持语言,而不必把一种表示当成唯一正式定义。

词法分析器生成器正是这条证明的工程化:解析 token 表达式,按结构生成 ε-NFA,合并规则后确定化,并标注接受态对应的 token 与优先级。闭包证明也会按运算挑选最自然的表示,再由 Kleene 定理把结论带回统一语言类。

参考资料
  • John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd ed., Pearson, 2006, Chapters 2–3.
  • Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013, §1.3.
关系图谱11 个相邻概念 · 2 类关系

拖动节点调整位置。

显示关系

显示:依赖

  1. 前置三跳
  2. 前置二跳
  3. 前置一跳
  4. 当前条目
  5. 后续一跳
  6. 后续二跳
  7. 后续三跳
文字版关系按与当前条目的最短距离分组
类型化关系

使用的工具