久しぶりに automaton

授業でやってるので。最初の年は List でやって「あんまり綺麗じゃない」、去年は Bool でやって「いろいろできたけど複雑」。

今年は、List Σ → Set で全部やるってのが降ってきて、確かに、わりと綺麗に。ただし、

　　簡単になったとは云いがたい

集合論の時にも Ordinal → Set でやるってのが降ってきて、いろいろ解決したわけですけどね。この

　　Set ってなんだよ

ってことだな。Agda 的には基本的な型でレベルがあるってくらいなんだが、何かの命題が入るという意味でもある。

言語、つまり、任意の入力文字のListの部分集合を List Σ → Set と書くわけですけど、その心は

　　Listの部分集合を識別する何かの述語がある

くらいだな。

　　is-a : List Σ → Set
　　is-a x = x ≡ (a ∷ [])

　　is-nil : List Σ → Set
　　is-nil x = x ≡ []

とやるわけですけどね。でも、Set は命題なので、それは証明しないと正しいとわからない。あるいは

　　is-nil? : (x : List Σ) → Dec ( x ≡ [] )

という x ≡ [] の証明があるかどうかを調べる述語を自分で実装するわけ。この場合なら

　　is-nil? [] = yes refl
　　is-nil? (_ ∷ _) = no (λ ())

とか。

だいぶ慣れたけど、いまでも、この Set 絡みは

　　まったくわかりません

となることがあります。