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

一般文法の閉包性質 -- 形式的検証

基本情報

論文ID: 2302.06420
タイトル: Closure Properties of General Grammars -- Formally Verified
著者: Martin Dvorak (オーストリア科学技術研究所)、Jasmin Blanchette (ルートヴィヒ・マクシミリアン大学ミュンヘン)
分類: cs.FL (形式言語とオートマタ理論)
発表会議: 第14回インタラクティブ定理証明国際会議 (ITP 2023)
論文リンク: https://arxiv.org/abs/2302.06420

要約

本論文はLean 3証明支援系を用いて一般文法(すなわちtype-0文法)を形式化した。著者は書き換え規則と文法から導出される単語の基本概念を定義し、文法を用いてtype-0言語のクラスが4つの操作下での閉包性を証明した:和集合、逆転、連接、およびKleene閉包。文献は主にチューリング機械の議論に焦点を当てており、これはより形式化が困難である可能性がある。Kleene閉包については、著者は文献に従うことができず、文法ベースの独自の構成を提案した。

研究背景と動機

問題背景

形式言語理論の重要性: 形式言語の概念はコンピュータ科学の中核であり、チューリング機械と形式文法を含む複数の形式主義を通じて認識可能である
type-0文法とチューリング機械の等価性: チューリング機械と一般文法は、再帰的可枚挙言語またはtype-0言語の同一クラスを特徴付ける
既存の形式化研究の限界: 証明支援系におけるチューリング機械の形式化に関する豊富な研究がある一方で、一般文法の形式化研究は相対的に不足している

研究動機

文法の利点: 一般文法はチューリング機械よりも定義が容易であり、一般文法に関する特定の証明はチューリング機械の類似性質の証明よりもはるかに単純である
閉包性質の重要性: type-0言語の閉包性質は形式言語理論の基礎的結果である
形式的検証の必要性: これらの基礎的結果の正確性を確保するため、機械検査可能な厳密な証明が必要である

核心的貢献

一般文法の初の完全形式化: Lean 3におけるtype-0文法の基本概念と操作の完全な定義
4つの閉包性質の形式化証明:
- 和集合に関する閉包性
- 逆転に関する閉包性
- 連接に関する閉包性
- 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