2003-06-01 [長年日記]
λ. なんつーか、やる気なくてすんません。
λ. 麻生さん勇気あるなー
λ. Hylomorphism
たまたま「CPO 連続関数」とかで検索してて見つかった http://www.ipl.t.u-tokyo.ac.jp/~murakami/lecture/caps2.pdf を読んだ。調べたかった事には全然関係なかったのだけど、Hylomorphismのところが気になった。Hylomorphismは最近読んだ長谷川立先生のチュートリアル「パラメトリック・ポリモルフィズム」で知って、そこでは
最後に,プログラム変換へのひとつの応用を述べておこう.始代数 μX.F(X) と終代数 νX.F(X) の等しさの応用である.この2つが等しいと,hylomorphism と呼ばれる技術を適用することができる.この論説ではちゃんと定義しなかったが,型A上の余帰納的定義(coinduction)から,A ⇒ νX.F(X) という関数が得られる.また,型B上の帰納的定義(induction)から,μX.F(X) ⇒ B という関数が得られる.いま,始代数と終代数は等しいとしているので,得られた2つの関数を合成することができ,A ⇒ B の型をもつ関数ができる.これを hylomorphism と呼ぶ.この技術のポイントは,関数の合成に際して受け渡される,μX.F(X) = νX.F(X) の型をもつ中間データが常に消去できることである.いわゆる融合規則の1つの場合である.
という風に説明してあったのだけど、ここでの
- 〚〛G,F: ∀A,B. (GA→A)×(F→G)×(B→FB) → (B→A)
- 〚φ,η,ψ〛G,F = μ(λf. φ ∘ η ∘ Ff ∘ ψ)
は、始代数と終代数の等しさも仮定してないし、全然違うものに見える。
……っと思ったけどそうでもないか。要は、始代数と終代数の等しさを仮定するかわりに、その間の自然変換を考えてるわけで、一般化になってるのか。ふむふむ……
[追記: この辺りの話については 2005-03-08 の日記を参照。]
お、『融合変換による関数プログラムの最適化』なんて論文もあるのか。GHCに実際に実装しているあたり、さすがに博士論文か。こっちも後で読もう。
ところで、圏論で通常用いる <f,g> や [f,g] のかわりに、f△g や f▽g のような表記を用いているのってプログラミング関係の論文でよく目にするけど、この表記法って一体誰が考えたのだろう? ちょっと気になる。
λ. FREESVG - Free PDF to SVG Conversion
PDFからSVGを作ってくれるサービス。chiko日記(2003-05-31)より。手元にあった幾つかのファイル(dvipdfmで作った)を試してみた限りではすべてエラーになってしまったのだけど、将来に期待。