マイヒル/ネロード(Myhill-Nerode*1)の定理については、このブログで何度か言及しています。
特に、「メイヤーオートマトンに関するマイヒル/ネロードの定理を宣伝する」では、表題のとおりに、メイヤーオートマトンとの関係においてマイヒル/ネロードの定理を説明しています。
メイヤーオートマトンの大きなメリット・魅力は、マイヒル/ネロード(Myhill-Nerode)の定理が成立することです。この定理の記述と証明は難しくないですが、先に、どんなありがたみがあるかを宣伝しておきます。
ここのメイヤーオートマトンとは、メイヤー先生の「Command-Query分離の原則」を満たすオートマトンのことです。「Command-Query分離の原則」は「ソフトウェアの正しさが判断できること」に繋がります。「正しさが判断できること」については次の記事に書きました。
強調されることが少ない(暗黙に仮定されること)ですが、CommandとQuery以外にConstructor(コンストラクタ)も必要です。上記の記事「ソフトウェアにとって大事なこと: 正しさが判断できること」で説明した「事前状況の制御可能性」と「事後状況の観測可能性」は、適切なConstructor-Command-Queryによって実現されます。また「挙動の予測可能性」における(予測のための)法則は、Constructor-Command-Queryを組み合わせて記述します。
というわけで、僕はマイヒル/ネロードの定理をソフトウェアシステムに関する非常に重要な定理と捉えているのですが、本来は形式言語理論の定理です。今まで、形式言語理論における(つまり元々の)マイヒル/ネロードの定理を述べたことがないので、このエントリーに書いてみようかと。
マイヒル/ネロードの定理はよく分からなかった
形式言語理論のマイヒル/ネロードの定理って、僕はよく分かりませんでした。「なんでこんなことを考えるのか?」とか「どうやってこの方法を思いついたか?」とか、そういう動機や背景が想像できないのです。教科書を追っていけば、マイヒル/ネロードの定理が実際に役に立つことは分かるのですが、「なんで?」という疑問が解消しないのです。「丸山善宏さんの「圏論的双対性の理論入門」と understanding conferrability」で紹介した丸山さんの言葉を使えば、explanationを追うことはできるが、understandingが得られない感じです。
以上が僕の正直な感想ですが、こんなことばかりゴチャゴチャ言っていると、肝心のステートメントが述べられないので、以下はドライな記述でいきます。
ステートメントのドライな記述
Aは記号の集合とします。形式言語理論では、Aをアルファベットと呼ぶのが普通です。Aの要素を、字(letter)とか記号(symbol)と呼びます。A* を“Aの要素の列”の集合(集合Aのクリーネスター)として、W = A* と置きます。Wの要素は文字列、語、文(string, word, sentence)などと呼ばれます。ここでは語と呼ぶことにします(なので、wordからWを使った)。
Wの要素、つまり語を α、β などのギリシャ文字小文字で表します。特にεは空語(空文字列)を意味する固有名詞として使います。Wは単なる集合ではなくて、語の連接をモノイド演算、εを単位元とするモノイドとなります。以下、このモノイド構造は仮定します。αとβの連接は、α・β または単に αβ と書きます。次のモノイド法則が成立します。
- (αβ)γ = α(βγ) (α, β, γ∈W)
- εα = αε = α (α∈W)
Wの部分集合Lを選んで固定します。Lはどんな集合でもかまいません。空集合でもいいし、L = W でもいいです。形式言語理論では、Wの部分集合を言語と呼ぶのですが、深い意味はなくて「Wの部分集合」の別な呼び名に過ぎません。この定義に深い意味を求たり、自然言語としての「言語」の先入観に拘るとロクなことはない、と注意しておきます。
さて、Wの部分集合であるLに対して、W上の同値関係≡を定義します。≡はLに対して決まるので≡Lのように書くべきですが、ここでは下付きLを省略します。
- α≡β とは、任意のξ∈Wに対して「αξ∈L ⇔ βξ∈L」であること。
論理式を使って書くなら、
- α≡β ⇔def ∀ξ∈W.(αξ∈L ⇔ βξ∈L)
この≡が実際に同値関係であることは簡単な練習問題ですね。
- α≡α
- α≡β ならば β≡α
- α≡β かつ β≡γ ならば α≡γ
同値関係≡は、Lによるネロード同値とか、単にL-同値とか呼ばれます。この同値関係≡こそがマイヒル/ネロードの定理のキモです。
Lによるネロード同値を用いて、次のように正規言語を特徴付けできます。
- Lが正規言語であることは、同値関係≡の同値類が有限個であることと同じ。
同値関係≡によるWの商集号を W/≡ と書くと:
- Lが正規言語である ⇔ W/≡ が有限集合
となります。
形式言語理論を超えた意義を持つマイヒル/ネロードの定理
以上に述べたように、マイヒル/ネロードの定理は正規言語に関する定理として述べられることが普通です。しかし、それはマイヒル/ネロードの定理の入り口に過ぎないと言えます。この入り口は、形式言語理論という“土地”からの入り口ですが、その入り口が適切かどうかもあやしいです。
ネロード同値の定義をみて、「なんでこんなことを考えるのか?」とか「どうやってこの方法を思いついたか?」って思いませんか、僕は疑問と違和感を感じました。今日は紹介しませんが、別の入り口のほうが(ある人々にとっては)自然かも知れません。
商集合 W/≡ は、オートマトン(状態遷移系)の状態空間と考えることができます。しかも、このオートマトンはWとLだけから標準的(canonical)に構成できます。でき上がったオートマトンはある種の普遍性を持ちます。マイヒル/ネロードの定理は、普遍的なオートマトンの構成法を与えているのです。
普遍的なオートマトン構成法としてのマイヒル/ネロードの定理という話題は、何年も前から書こうとしていて先延ばしになっている話題なんですよね。「メイヤーオートマトンに関するマイヒル/ネロードの定理を宣伝する」でその「ありがたみ」はけっこう書いたのですが、内実が書いてないです。今回は、本来の(だが一側面に過ぎない)形である形式言語理論におけるマイヒル/ネロードの定理について書きました。いつか、内実と全貌を記述したいとは思っています。
*1:Nerodeは「ネローデ」とカタカナ書きされることもあります。