日々の流転

λ. Guarded Induction on Final Coalgebras. Duško Pavlović

guarded (co)induction に対して圏論的なモデルを構成しているのだが……結構複雑だな。もっとシンプルなものを期待していたので驚いた。これはこれで興味深いけど、とりあえず深入りしないことにしよう。

それと、興味深く思ったのは、以下のような視点というか考え方。

In fact, the most interesting conceptual distinctions often begin to surface only when the symmetry starts breaking down. Going back to monads and comonads, recall, e.g., how the free algebras for a monad form an algebra classifier (the clone), whereas the cofree coalgebras for a comonad do not seem to either classify or “coclassify” anything meaningful. And indeed, the former turns out to be the foundation of a rich mathematical theory, capturing algebraic varieties by functorial semantics, whereas the latter remains a symptom of the fundamental fact that this theory does not have a dual: coalgebras for comonads on toposes tend to form toposes again, rather than “covarieties”.

私も含めて圏論ユーザは双対性を圏論を強力な武器と認識していて、双対性が利いてくるような状況には興味を示すけど、双対性が役に立たないような状況には比較的興味を示さないことが多いです。でも、そういう状況でこそ見えてくる興味深い点というのもあるんだなぁ。反省、反省。

• <URL:http://www.kestrel.edu/home/people/pavlovic/coalgebra.html>
• <URL:http://dx.doi.org/10.1016/S1571-0661(04)00056-8>
• citeseer:pavlovic98guarded.html

分からなかった点など

• p.3 で　tree induction, stream induction, labelled tree induction と呼んでいるのは何を指している?　inductionという言葉をどういう意味で使っているのか正確な定義が知りたい。
• p.7 の F=P_Σ のときの、prefixing operations が変な気がする。Σの部分集合の個数だけあるのでは?
• p.6 の 「But !: γ is surely an epi, because it is split by fix (be it unique or not). So ∂ induces a unique prefix η1, and η1 induces a unix fixpoint fix.」という部分が良く分からない。epiだと何故uniqueに?