オートマトンの続き

subset construction かなりはまっていて、木で明示的に状態を記録していく方法で、一応、書けたんですが

　　まったく動く気がせず

で、すべての状態の組合せに対して次の状態の組合せを生成する関数を作れば良いんじゃないか? と思いついていて、それで書き直したら朝飯前に終わりました。

状態の組合せって、状態の集合Qからtrue/falseへの写像だから、

　　 Q → Bool

これでいいわけね。NFAは、

　　record NAutomaton ( Q : Set ) ( Σ : Set　)
　　　　　 : Set　where
　　　　field
　　　　　　　nδ : Q → Σ → List Q
　　　　　　　sid : Q　→　ℕ
　　　　　　　nstart : Q
　　　　　　　nend　: Q → Bool

なので、生成するDFAの状態遷移は

　　　(Q → Bool) → Σ → (Q → Bool)

こんな感じ。なので、

　　δconv : { Q : Set } { Σ : Set　} { n　: ℕ }　→ FiniteSet Q n →　
　　　　( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)

を書けば良いというわけ。Q は有限だから ℕ に対応するというのを使って、

　　exists N ( λ r → list2sbst N (nδ r i) q )

なんか一行で書けるのか。

なんとなく実装よりに木とかリストとか使ってしまうけど、関数で書いていく方が Agda 向きならしい。

まだ、いろいろやることありますが、だいたいこの方向でいけそう。そろそろシラバス書かないとな。

regex からの変換も書き終わった。 あとは、

　　regex の拡張とバックトラック
　　ω automaton ( 停止しないオートマトン)
　　CTL (computation tree logic) を使ったモデル検査
　　characteristic function
　　push/down
　　2 stack automaton ( = turing machine)
　　turing machine の停止性
　　P と NP

ぐらいまでやる予定です。