形式语言与自动机可视化实验室
通过 8 个可交互的 SVG 可视化模块，直观理解确定性 / 非确定性有限自动机、Thompson 构造、下推自动机、图灵机、乔姆斯基层级、泵引理与 DFA 最小化等核心理论。从状态转移图到带读写头的磁带，从 ε 闭包到 Hopcroft 划分细化，零依赖、纯前端。
DFA 确定性有限自动机
一个 DFA 由状态集、输入字母表、转移函数、起始状态与接受状态构成。每个状态对每个输入符号有且仅有一个确定的后继。下方自动机识别以 "01" 结尾的二进制串，逐步执行可看到当前状态高亮与走过的转移路径。
NFA 非确定性有限自动机
NFA 允许同一状态对同一输入有多个后继，并支持 ε 转移。执行时同时维护多个活跃状态集合（ε 闭包）。下方 NFA 用 ε 转移识别包含子串 "01" 的串，可切换查看经子集构造得到的等价 DFA。
正则表达式转 NFA
Thompson 构造将正则表达式递归地转换为带 ε 转移的 NFA：字符、连接、并 (|)、Kleene 星 (*) 各有固定模式。下方可输入正则并切换 NFA / DFA 视图，输入测试串后高亮匹配时经过的活跃状态。
下推自动机 PDA
PDA 在有限状态机基础上增加一个下推栈，栈顶符号与输入共同决定转移：可压入 (push) 或弹出 (pop)。下方 PDA 通过配对的压入 / 弹出来识别平衡括号串，逐步执行可看到栈的实时变化与接受条件。
图灵机 Turing Machine
图灵机拥有可读写的双向无限磁带与读写头：每步根据当前状态与磁带头所指符号写入新符号、移动磁头并切换状态。下方机器通过标记配对 a/b 来识别 aⁿbⁿ，逐步运行可观察磁带内容、读写头位置与状态演变。
乔姆斯基层级
乔姆斯基于 1956 年将文法按生成能力分为四层：3 型（正则）⊂ 2 型（上下文无关）⊂ 1 型（上下文敏感）⊂ 0 型（无限制）。每层对应一类自动机。下方以嵌套集合展示包含关系，选择类型可查看对应文法与示例语言。
泵引理 Pumping Lemma
泵引理给出语言属于某类的必要条件：对足够长的串 w，存在分解 w = xyz，使得 xyⁱz 仍在语言中。下方以 aⁿbⁿ 为反例演示正则泵引理——当 y 全为 a 时，反复泵入会破坏 a/b 数量相等，从而证明该语言非正则。
自动机最小化
每个正则语言都存在唯一的最小 DFA。Hopcroft 算法从接受 / 非接受两组划分出发，反复细化：若同组状态在某输入下转移到不同组则分裂。下方逐步展示划分细化，直到稳定得到最小自动机。