トップ «前の日記(2004-06-28) 最新 次の日記(2004-06-30)» 月表示 編集

日々の流転


2004-06-29 [長年日記]

λ. 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追記] この論文で使ってるdifunctordinatural transformationはあまりメジャーな概念ではないし、この論文では明示的に定義していないので、自明とは思うが念のため自分の理解した定義を書いておこう。

difunctor F
bifunctor F: C×Cop→D
difunctor F,G: C×Cop→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 として抽象化する事が出来る。

*1 もっと良い方法があったら教えてください!

λ. ODA

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

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

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

NHKにようこそ! (1) (角川コミックス・エース)(滝本 竜彦/大岩 ケンヂ)

Tags:
本日のツッコミ(全3件) [ツッコミを入れる]
ψ takot (2004-06-30 22:13)

Hagino [Hag87]って,萩野先生のD論じゃないっすか(笑)

ψ shelarcy (2004-06-30 23:35)

Category かぁ。すっきり纏まっているけど、初めて見る人には辛いものがあります。

ψ さかい (2004-07-01 15:04)

> takot<br><br>そうですよ〜 (笑)<br><br>> shelarcy<br><br>計算機科学で使う圏論なんてたかが知れていて、圏論のそんな深遠な部分は大抵は必要ないです。初めて見る人にとって辛いというのも分かりますが、単に慣れの問題だと思います。