日々の流転

λ. V. Vene. Categorical programming with inductive and coinductive types. Diss. Math. Uni. Tartuensis, v. 23, Uni. of Tartu, Aug. 2000. - .ps.gz, .pdf.

を読んだ。catamorphism, anamorphism, paramorphism, apomorphism, histomorphism, futumorphism といった再帰のパターンについて、とても良くまとまっている。catamorphismとanamorphismは有名だし、他の4つについても知ってる人はいると思うけど、こういう形で纏まっていると何かと嬉しい。それから、Mendler-style algebra を使ったアプローチも面白かった。

些細な点だが何点か気になる点もあった。例えば The categorical treatment of inductive and coinductive types as initial algebras and terminal coalgebras for covariant functors comes from Hagino [Hag87], who designed a typed functional language CPL based on distributive categories and initial algebras and terminal coalgebras for strong covariant functors. と書いてあるけど、based on distributive categories and initial algebras and terminal coalgebras for strong covariant functors.というのはCPLの特徴ではなくてCharityの特徴のはず。

[2004-07-08追記] この論文で使ってるdifunctorとdinatural transformationはあまりメジャーな概念ではないし、この論文では明示的に定義していないので、自明とは思うが念のため自分の理解した定義を書いておこう。

difunctor F

bifunctor F: C×C^op→D

difunctor F,G: C×C^op→D の間の dinatural transformation φ: F→G

{φ_A: F(A,A)→G(A,A)}_A∈C で ∀A,B∈C,f:A→B について以下の図が可換。

         F(I,f)        F(f,I)
  F(A,A) ←── F(A,B) ──→ F(B,B)
     │                          │
φ_A │                          │φ_B
     ↓                          ↓
  G(A,A) ──→ G(B,A) ←── G(B,B)
         G(f,I)        G(I,f) 

[2004-07-12追記] 5.2 でのAlg(F)^mとAlg(F)が同型であることの証明だが、 米田の補題の自然同型をη_C,F: hom(hom(-,C),F) → F(C) とすると、 全ての h: A→B について下図が可換になり、 ここからAlg(F)^m とAlg(F)が同型であることは直ちに言える。

                                 η_{A,hom(F(-),A)}
     hom(hom(-,A), hom(F(-),A)) ─────────→ hom(F(A),A)
                 │                                       │
hom(hom(-,A),    │                                       │hom(F(A),h)
    hom(F(-),h)) │                                       │
                 ↓              η_{A,hom(F(-),B)}       ↓
     hom(hom(-,A), hom(F(-),B)) ─────────→ hom(F(A),B)
                 ↑                                       ↑
hom(hom(-,h),    │                                       │hom(F(h),B)
    hom(F(-),B)) │                                       │
                 │                                       │
     hom(hom(-,B), hom(F(-),B)) ─────────→ hom(F(B),B)
                                 η_{B,hom(F(-),B)}

For a reader versed in category theory, the result is a consequence from the Yoneda lemma. と書いてあったが、確かに米田の補題を知っていればこっちの方が分かりやすいな。

[2005-02-24 追記] この論文に出てくるような記法を LaTeX でするには、以下のようなマクロを用意しておけばよいのかな*1。

\def\cata#1{(\!|#1|\!)}
\def\ana#1{\lbrack\!(#1)\!\rbrack}
\def\para#1{\langle\!|#1|\!\rangle}
\def\apo#1{\lbrack\!\langle#1\rangle\!\rbrack}
\def\histo#1{\{\!|#1|\!\}}
\def\futu#1{\lbrack\!\{#1\}\!\rbrack}

[追記] ここで述べられている再帰のパターンは Comonadic Iteration と Monadic Coiteration として抽象化する事が出来る。

λ. ODA

某所で「ODAよりもNGOの活動の支援に税金を使った方が有益では?」的な意見を見て、ちと頭が痛くなる。実際にはNGOへの援助もODAの一部として実施されているのに……

λ. 『NHKにようこそ!』, 滝本 竜彦 [原作] 大岩 ケンヂ [画]

を読んだ。こういうダメな漫画大好きですよ。