正規言語の零壱則
たまには正規言語の研究の話を.今年パリで証明した定理について紹介します.
どのような定理かざっくりカジュアルに言うと
正規言語が「ほとんど全ての文字列を含む」または「ほとんど全ての文字列を含まない」⇔ を受理する代数構造が零元を持つ ⇔ を受理する最小オートマトンが特別な形をしている
ということを示しました.
「カジュアルに」と書いてみたものの,自分で読んでみてもなかなか意味不明です.もうちょっときっちりフォーマルに説明してみましょう.
正規言語の零壱則
零壱則(zero-one law)とは,ある種の事象が「確率1で起こる(確実に起こる)」か「確率0で起こる(確実に起こらない)」という両極端な振る舞いを示す時に使われる言葉です.
零壱則という名前は一般的なもので,「XXXの零壱則(XXX's zero-one law)」という名前の定理や事実がWikipediaにはいくつか列挙されています.
Zero–one law - Wikipedia, the free encyclopedia
It may refer to:
- Borel–Cantelli lemma
- Blumenthal's zero–one law for Markov processes,
- Engelbert–Schmidt zero–one law for continuous, nondecreasing additive functionals of Brownian motion,
- Hewitt–Savage zero–one law for exchangeable sequences,
- Kolmogorov's zero–one law for the tail σ-algebra,
- Lévy's zero–one law, related to martingale convergence.
- topological zero–one law related to meager sets
今回紹介するのは「正規言語の零壱則」です.有限の文字集合をとし,上の全ての有限長文字列の集合をで,長さ全ての文字列の集合をで表します.上の正規言語に対して確率関数を次のように定義します:
\begin{align} \displaystyle \mu_n(L) = \frac{|L \cap A^n|}{|A^n|} = \frac{|L \cap A^n|}{|A|^n}. \end{align}
この関数は「長さnの文字列集合からランダムに取ってきた文字列がに属している確率」を表していることが分かります.
さて,ある正規言語について,上で定義した確率関数の極限が0か1に収束するとき,つまりのとき,正規言語は零壱則に従うと呼ぶことにしましょう.直感的には正規言語が零壱則を満たすとはが「ほとんど全ての文字列を含む」または「ほとんど全ての文字列を含まない」と考えることができます.
零壱則の決定可能性について
さてさて,ここで定義した正規言語の零壱則は決定可能な性質,つまり「与えられた正規言語が零壱則に従うかどうか」を判定するアルゴリズムはあるのでしょうか? いかにもありそうです.実際それを求めたのが今回の定理なのですが,それを説明するためにもうちょっと用語を整理する必要があります.
統語半群
正規言語が(決定性)有限オートマトンで特徴付けられることは広く知られています.(この辺が良くわからないという人は拙著『正規表現技術入門』をどうぞ :-)
正規表現技術入門 ――最新エンジン実装と理論的背景 (WEB+DB PRESS plus)
- 作者: 新屋良磨,鈴木勇介,高田謙
- 出版社/メーカー: 技術評論社
- 発売日: 2015/04/14
- メディア: 単行本(ソフトカバー)
- この商品を含むブログ (1件) を見る
一方, 正規言語が有限モノイドでも特徴付けられるということはあまり知られていません(この代数的特徴付けも『正規表現技術入門』の巻末付録にて解説されています).
モノイドとは結合則を満たす二項演算と単位元を持った代数構造で,群から「逆元の条件」を取り払ったモノです.例えば文字列の集合も「2つの文字列を結合して1つの文字列にする操作」を二項演算として考えるとモノイド構造が入ります.この場合の単位元は空文字列です.
さて,正規言語Lから有限オートマトンを具体的に構成することができるように,言語LからLに対応する特別なモノイド -- 統語半群(syntactic monoid)*1 を次のように構成することができます:
\begin{align} M = A^* / \sim_L. \end{align}
ここでは言語によって定まる上の同値関係:
\begin{align} u \sim_L v \Leftrightarrow \forall x,y \in A^* [ xuy \in L \Leftrightarrow xvy \in L ] \end{align}
で, は文字列の集合(無限モノイド)をで割ったモノイドです.有名なMyhill-Nerodeの定理は言語の正規性をこの統語半群の有限性で特徴付ける綺麗な定理です.
定理(Myhill-Nerode)
言語が正規 ⇔ の統語半群が有限.
さて,これで正規言語の零壱則について説明する道具が駆け足ながら揃いました.
主定理
定理1(正規言語の零壱則)
正規言語について以下の3つの条件は等しい:
- が零壱則に従う
- の統語半群が零元を持つ
- の最小オートマトンが零オートマトン
ここで言うモノイドのの零元とは,次の条件を満たすのある元のことです:
\begin{align} \forall m \in M [xm = mx = x]. \end{align}
例えば整数と掛け算の成すモノイドは数のが零元となります.には何を掛けても,そのまんまですね.
確率関数 の極限が0か1に収束するという条件(1)と統語半群に零元が存在するという条件(2)とが同値というのが意外かもしれません.条件(2)から条件(1)を示すのは容易なのですが,その逆を示すのがなかなか難しいです.
実際の証明では条件(3)の零壱則のオートマトン的特徴付け(零オートマトン)をうまく活用して「条件(2)⇒条件(3)⇒条件(1)」を示しました(零オートマトンの定義はちょっとややこしいので割愛します).条件(3)から条件(1)を示すのが証明の一番面白いところで,零壱則を満たす言語族の閉包性とEilenbergによる正規言語のVariety Theoremの核となる補題を...... 証明の詳細はGandALF'15という国際会議に採択された拙文"An Automata Theoretic Approach to the Zero-One Law for Regular Languages: Algorithmic and Logical Aspects"にてご確認ください.
今年パリで示した定理の論文がGandALF'15に採択されました. 「正規言語Lがほとんど全ての文字列を含む/含まない(零壱則に従う) ⇔ Lのsyntactic monoidが零元を持つ」というカッコいい定理(私見)です. http://t.co/dUID7MyzSP
— Ryoma Sin'ya (@sinya8282) 2015, 8月 8
統語半群は正規言語から具体的に構成でき,零元があるかどうかも判定することができるため,定理1は正規言語の零壱則が決定可能な性質であることを導きます.
有限グラフの零壱則
そもそも零壱則に興味を持ったのは,去年輪講*2した"Elements of Finite Model Theory"に載っていた有限グラフ零壱則を特徴づけるFaginの定理がきっかけでした.
定理(Fagin)
一階述語論理式がほとんど全ての有限グラフで成り立つ(i.e. ) ⇔ がランダムグラフで成り立つ.
ここでいうランダムグラフとはある特別な無限グラフです.ランダムグラフはいくつかの異なる,しかし等価な構成法がしられており,構成法の提案者の名前を取ってErdős–RényiグラフやRadoグラフとも呼ばれたりします.
このFaginの定理は有限グラフの零壱則の決定可能な特徴付けにもなっています.このFaginの定理のように綺麗な定理が有限文字列の零壱則 -- すなわち正規言語の零壱則でも成り立たないか?と考えるのは自然なことのように思えます.
有限グラフの零壱則とFaginの定理,正規言語と論理の関係について詳しく知りたい!という人はぜひ Elements of Finite Model Theory を読むことをお勧めします.僕は論理やモデル理論の知識が全くない状態からこの書籍を輪講しましたが,説明が丁寧で飛躍が無くとてもわかり易かったです.有限モデル理論の良い入門書だと思います*3.
Elements of Finite Model Theory (Texts in Theoretical Computer Science. An EATCS Series)
- 作者: Leonid Libkin
- 出版社/メーカー: Springer
- 発売日: 2004/07/02
- メディア: ハードカバー
- この商品を含むブログを見る