coinduction

論理、特に演繹系は、命題と命題を結ぶ矢印である推論からなる圏になるわけですが、

　　矢印を全部反対にすると双対圏が得られる

ってのあります。

数学的帰納法を induction というわけだけど、その矢印を全部逆にしたのが coinduction 。逆帰納法かな?

AIM で Automaton の構成を見せたら、いや、有限性抜きでできるんだよと論文送ってもらったんですが、それが、 coinduction でした。

その辺、あんまり近寄りたくなかったんだっけどな。逆数学とか。まぁ、圏論触ったから仕方ないか。

数学的帰納法は、p(0) を示して、p(n+1) を p(n) から示すみたいな感じ。実際には証明するのはp(n)だから、

　　p(0) = ?　
　　p(s(n)) = ? p(n)

と言う感じで、data (場合分けされたデータ構造)を分解しながら処理していく感じ。

そうすれば、問題は一段小さくなるから、小さい部分では証明はできてるから再帰で。

coinduction だと、徐々に record で表される直積で作られたデータ構造を構築していく感じ。終わりは自分で終わりという。

オートマトンの言語(文字列の部分集合)だと、

　　　　record　Lang (i : Size)　: Set　where
　　　　　 coinductive
　　　　　 field
　　　　　　　ν : Bool
　　　　　　　δ : ∀{j : Size< i} → A → Lang j

こんな感じ。文字列なのに List とかない。Size は Agda に coinduction の停止性を教えるためのものらしい。A は仮定された文字の集合。

文字を与えると、δ (derivative 微分か?) 新しい少し小さい Lang j が作られて、もう終わりにしたい時には ν で判定する感じ。

　　　　_∋_ : ∀{i} → Lang i → List i A → Bool
　　　　l ∋ [] = ν l
　　　　l ∋ ( a ∷ as ) = δ l a ∋ as

単なるListではなく長さを持つ List を自分で作らないといけないらしい。 δ l a 自体が状態だと思えば、状態遷移そのもの。

確かに、Automaton と相性が良い。逆に、 List i A → Bool が与えられたら、

　　　　trie : ∀{i}　(f : List i A → Bool) → Lang i
　　　　ν (trie f) = f []
　　　　δ (trie f) a = trie (λ as → f (a ∷ as))

という風に作れば良いらしい。f の引数がどんどん貯まっていく感じだな。実際には f は有限状態だから、部分評価できると考えれば良い。

　　　 trie f = record { ν = f [] ; δ = λ a → trie (λ as → f (a ∷ as)) }

を、こんな風にかけるのか。いろいろあるな。

で、状態を明示したければ、

　　record DA (S : Set) : Set where
　　　　field ν : (s : S) → Bool
　　　　　　　δ : (s : S)(a : A) → S

　　lang : ∀{i} {S} (da : DA S) (s : S) → Lang i
　　Lang.ν (lang da s) = DA.ν da s
　　Lang.δ (lang da s) a = lang da (DA.δ da s a)

こんな風にするらしい。Size はどこにいった? 初期状態はDAそのものなのか。NDA はこれから考えます。