Subset Construction

なんか去年苦労してた気がするんだが... NFAからDFAを作るってやつですね。作ったものが元と一致する証明さぼってたんですが...

授業が終わった後、書いてみたら一発だった。どういうこと。やっぱり、Agda力が上がってるってことか。

　　　　(NAutomaton Q　Σ ) → (astart : Q ) → (Automaton (Q → Bool)　Σ )

状態Qの非決定性オートマトンを、状態(Q→Bool)な決定性オートマトンに読み替えるだけだから、入力をたどれば一致することは自明。

FiniteSet は Q が Fin n (0..n)に isomorphic (1対1)だってのですが、ちょっとださいかな。

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