2025-11-23T10:13:16.980830

Closure Properties of General Grammars -- Formally Verified

Dvorak, Blanchette

We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.

academic

Closure Properties of General Grammars -- Formally Verified

基本信息

论文ID: 2302.06420
标题: Closure Properties of General Grammars -- Formally Verified
作者: Martin Dvorak (Institute of Science and Technology Austria), Jasmin Blanchette (Ludwig-Maximilians-Universität München)
分类: cs.FL (Formal Languages and Automata Theory)
发表会议: 14th International Conference on Interactive Theorem Proving (ITP 2023)
论文链接: https://arxiv.org/abs/2302.06420

摘要

本文使用Lean 3证明助手形式化了通用语法(即type-0语法)。作者定义了重写规则和由语法派生的单词的基本概念，并使用语法证明了type-0语言类在四种操作下的封闭性：并集、逆转、连接和Kleene星运算。文献主要关注图灵机论证，这可能更难形式化。对于Kleene星运算，作者无法遵循文献并提出了自己的基于语法的构造。

研究背景与动机

问题背景

形式语言理论的重要性: 形式语言概念是计算机科学的核心，可以通过多种形式主义来识别，包括图灵机和形式语法
type-0语法与图灵机的等价性: 图灵机和通用语法都刻画了递归可枚举语言或type-0语言的同一类别
现有形式化工作的局限: 已有大量关于图灵机在证明助手中形式化的工作，但通用语法的形式化工作相对缺乏

研究动机

语法的优势: 通用语法比图灵机更容易定义，某些关于通用语法的证明比图灵机的类似性质证明要简单得多
封闭性质的重要性: type-0语言的封闭性质是形式语言理论的基础结果
形式化验证的需求: 需要机器检查的严格证明来确保这些基础结果的正确性

核心贡献

首次形式化通用语法: 在Lean 3中完整定义了type-0语法的基本概念和操作
四个封闭性质的形式化证明:
- 并集封闭性
- 逆转封闭性
- 连接封闭性
- Kleene星运算封闭性
创新的Kleene星构造: 由于文献缺乏基于语法的构造，作者发明了自己的语法基础构造方法
可重用的抽象框架: 开发了lifted_grammar结构来减少重复代码并提供通用的证明模式
约12,500行的开源Lean代码库: 提供完整的形式化实现供社区使用

方法详解

基础定义结构

符号系统

inductive symbol (T : Type) (N : Type)
| terminal : T → symbol  
| nonterminal : N → symbol

语法规则表示

structure grule (T : Type) (N : Type) :=
( input_L : list (symbol T N))
( input_N : N)  
( input_R : list (symbol T N))
( output_string : list (symbol T N))

语法定义

structure grammar (T : Type) :=
(nt : Type)
(initial : nt)
(rules : list (grule T nt))

核心操作定义

语法变换关系

def grammar_transforms (g : grammar T) (w1 w2 : list (symbol T g.nt)) : Prop :=
∃ r : grule T g.nt,
  r ∈ g.rules ∧
  ∃ u v : list (symbol T g.nt),
    w1 = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v ∧
    w2 = u ++ r.output_string ++ v

派生关系

def grammar_derives (g : grammar T) : 
  list (symbol T g.nt) → list (symbol T g.nt) → Prop :=
relation.refl_trans_gen (grammar_transforms g)

技术创新点

1. lifted_grammar抽象框架

为了减少重复代码，作者开发了一个抽象结构：

包含较小语法g0和较大语法g
提供lift_nt和sink_nt函数在不同非终结符类型间转换
确保注入性和对应规则的正确性

2. 连接操作的创新处理

传统的上下文无关语法连接构造在通用语法中失效。作者的解决方案：

为每个终结符创建代理非终结符
确保g1和g2使用的非终结符完全分离
避免跨连接边界的字符串匹配问题

3. Kleene星的原创构造

由于文献缺乏基于语法的构造，作者发明了新方法：

引入分隔符#来构建隔离单词的"隔间"
使用清理器R从头到尾遍历并移除分隔符
新规则集：P* = P ∪ {Z → ZS#, Z → R#, R# → R, R# → ε} ∪ {Rt → tR | t ∈ T}

实验设置

形式化环境

证明助手: Lean 3
数学库: mathlib
代码规模: 约12,500行格式良好的Lean代码
元编程: 使用Lean的元编程框架开发小规模自动化

验证方法

结构归纳: 对派生关系使用结构归纳证明
案例分析: 对不同规则应用情况进行详尽的案例分析
不变量维护: 在复杂证明中维护关键不变量

实验结果

主要定理

并集封闭性: theorem T0_of_T0_u_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 + L2)
逆转封闭性: theorem T0_of_reverse_T0 (L : language T) : is_T0 L → is_T0 (reverse_lang L)
连接封闭性: theorem T0_of_T0_c_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 * L2)
Kleene星封闭性: theorem T0_of_star_T0 (L : language T) : is_T0 L → is_T0 L.star