Automaton

後期の授業用に、Automaton を Agda で書いてたりするんですが... まぁ、割と簡単に書けるんだけど、

　　簡単なものはな

先に進んでいくと、どうしても複雑になってしまって。

　　DFA
　　NFA
　　Regular Expression
　　εNFA
　　subset construction

で一通りなはずです。これだと、Agda でやるからわかりやすいってわけでもないな。まぁ、だいたいそんなものなんだけど。

εNFA は複数の状態を何もなくても渡り歩くε遷移ってのがあるんだけど、正規表現からAutomatonに変換するのにad-hocに使うものなのね。

前に書いた時には、もちろんε遷移とか使わないで書くのでそれが当然だと思っていたんですが、そうすると、かなり複雑になる。と言っても、倍は違わないんだが。

ε遷移は遷移する状態で閉包を作ってしまえば良くて、それは状態の集合なので、subset construction にはほとんど影響がないらしいです。

ただ、思ったより複雑なので、Regular Expressionが生成する文字列を変換したεNFAが受け付ける証明とかは結構でかそうだな。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/