Finite Set

今週末は、Agda でそんなのやってました。首里で Ingress で遊ぼうと思っていたのに。結婚式の帰りは公栄あたりを廻ってました。

NFAの受理を調べるのに、有限集合から検索ってのをやるので、書いたんですが、Agda だと

　　Data.Fin

だけでやるものかも。これにdata とか、いろんな集合(Agdaでは関数の型だ)を対応させるわけ。

Automaton だけでも、Finite Set の和集合、'積集合、Q → Bool と一通りでてきてしまう。個数はそれぞれ、足し算、掛け算、exp 2 になります。

その結果が、Data.Fin つまり個数制限のある自然数に写像されるわけだ。小学生でもわかる内容なんですが...

これが思ったより、はまる。Data.Fin との写像には「ちゃんと範囲に収まっている」というのを示す論理式があって、それを持ち歩くことに。

それに対する ISO つまり、

　　record ISO (A B : Set) : Set where
　　　 field
　　　　　 A←B : B → A
　　　　　 B←A : A → B
　　　　　 iso← : (q : A) → A←B ( B←A q ) ≡ q
　　　　　 iso→ : (f : B) → B←A ( A←B f ) ≡ f

を確認することに。超絶面倒くさいです。

和集合とか仮定してすませてたんですが、まぁ、そういうわけにもいかないかと思って始めたんですが、結構難しい。

和集合は足し算なので、Data.Finの加減算と格闘する羽目に。ほとんどできたんですが、そこで、

　　要素を一つ付け加える操作を∨で定義して
　　それをn回繰り返して、A ∨ Fin n を作り
　　Fin n に B を対応させる

というのを思いついた。ISOがあれば同じ Finite Set だからな。これで、加減算とはほぼおさらばできた。素晴らしい。

和集合ができれば、積も同じように、∨をn回繰り返せば良い。

次は、Q → Bool ですが、List Bool でも良い。これも空列から始めて、一つ増えると、∨で倍に。倍々なので exp 2 。わかりやすい。

なんですが、Q → Bool と List Bool のISOが難しかった。プログラマって、

　　要求される入力よりも広い範囲の入力を受け付ける関数

を書くよね。でも、これが ISO の範囲をはずれて調べる羽目に。当然、そこではISOは成立しない。

結局、範囲を正確に受けとる関数に変換する羽目に。しかも、行きと帰りと両方。

これで、Q → Bool までできた。

そこで終わりにすれば良かったんですが、部分集合欲しいなと思って。m 個の Finite Set から n < m 個のFinite Set を作るわけですが...

個々の要素を Q と Q に付いている番号が n よりも小さい条件を一緒に持ち歩けばよい。結果的には、

　　data fin-less { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
　　　elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less n<m fa

というdataを持ち歩けば良いわけですが、A←B で生成した条件を、iso← 側で検算することになる。そこその大きさの項を検算する羽目に。

そこで、積やListと同じでzeroから増やす方法もやってみたのですが、複雑はほぼ変わらない。まぁ、どの方法でもできそうなところまではいったのだが。

結局、この data に対する合同条件

　　get-elm : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → fin-less n<m fa → A
　　get-elm (elm1 a _ ) = a

　　get-< : { n m : ℕ } {n<m : n < m } { A : Set } {fa : FiniteSet A {m}} → (f : fin-less n<m fa ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
　　get-< (elm1 _ b ) = b

　　fin-less-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
　　　 → (x y : fin-less n<m fa ) → get-elm {n} {m} {n<m} {A} {fa} x ≡ get-elm {n} {m} {n<m} {A} {fa} y → get-< x ≅　get-< y → x ≡ y
　　fin-less-cong n<m fa (elm1 elm x) (elm1 elm x) refl HE.refl = refl

を書いて頑張って検算する方法でできた。

ここでわかったのは、この fin-less の data は、集合のLimitiを作るものと同じ。Data.Fin の構造を保つ部分集合を作るということは、結局は、'

　　圏のLimit、つまり、随伴関手

を作ることと同じことらしい。どうりで難しいわけだよ。

結果的には割と短い証明でできたので良しと言うことにしよう。


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