Automaton の結合

Automaton で受理される言語(文字列の集合)の個々のものをつなげたものを受理するAutomatonがあるって話。

途中でどこでわければ良いかわからないから非決定性Automatonを導入するってやつです。で、非決定性Automatonは決定性に変換できるから証明終了と。

なんだけど、ちょっと待て。確かに非決定性Automatonは作ったけど、それが正規言語AとBの結合に等しい言語を定義しているかどうかは調べてないよね。

いや、確かに、図を見ると自明なんですが。でも、そもそも非決定性Automatonの受理のルールが複雑だからなぁ。

で、実際に Agda で証明に行くわけですが、予想通り、かなりはまった。

　　split : {Σ : Set} → (List Σ → Bool)
　　　　　→ ( List Σ → Bool) → List Σ → Bool
　　split x y　[] = x [] /\ y []
　　split x y (h　∷ t) = (x [] /\ y (h　∷ t)) \/
　　　split (λ t1 → x (　h ∷ t1 ))　(λ t2 → y t2 ) t

　　Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
　　Concat {Σ} A B = split A B

こんな感じで言語の結合は定義できるわけですが、 contain A x で Automaton A が x 受理するとして、

　　closed-in-concat :　{Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )

こんな感じで Concat が、でっちあげたNFA である M-Concat A B と等しいことを見に行きます。すると、

　　　(1) closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true

と

　　　(2) closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true

とを示すことになる。まぁ、そうだよな。

finiteSet 有限集合の∃関連の述語は一通り書いたし、split の逆とか使って、(1)はスムースだった。仮定から二つの入力が
あるのがわかるので、それが実際に受理されることを NFA をたどって示せばよい。

なんですが、(2)が良くわからない。

　　　ずーっと A で動いていて、Aが終わりで残りが B なら Ok

つまり、A until B 見たいな時相論理式を証明にいくわけだな。

　　aend (automaton A) qa) /\　accept (automaton B) (δ (automaton B) (astart B) h) t

を調べて真なら、それで成立。成り立たなかったら次の状態に進む。

なんだけど、M-Concat A B が非決定的なので、

　　　途中、B になりそうになるが、いつか B でなくなる

ってのがある。つまり、 accept (automaton B) s x ってのが、その時点では判明しない。この辺、専門なはずなんだけどな。

　　ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
　　ab-case (case1 qa') qa x = qa'　≡ qa
　　ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x　≡ true )

　　contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
　　　　　→ (qa : states A )　→ (　(q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )

とかいうのを思いついて、ようやっと突破できた。

いや、でも、ちょっと複雑すぎるだろ。NFAに閉じれば簡単になるかも。co-induction とか使えれば面白いんだが。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/regular-language.agda