ヒビルテ(06-01[長年日記])

たまたま「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 のような表記を用いているのってプログラミング関係の論文でよく目にするけど、この表記法って一体誰が考えたのだろう? ちょっと気になる。

Tags: 圏論

λ. FREESVG - Free PDF to SVG Conversion

PDFからSVGを作ってくれるサービス。chiko日記(2003-05-31)より。手元にあった幾つかのファイル(dvipdfmで作った)を試してみた限りではすべてエラーになってしまったのだけど、将来に期待。

Tags: URL

λ. ダブル・ジョパディ

を見た。

Tags: 映画

[ツッコミを入れる]

2005-06-01

λ. Monadius - a scientist's toy box

メモ。

グラディウスを知らないので何とも言えないけど、普通に難しいね。あと、コンティニューしても最弱装備で再開なのですぐやられてしまうし、コンティニューの意味があんまし無い気がした。

(1,1)-(2,3).00154420pts.replay

Tags: haskell

λ. 投票による結果報告

投票COが有りならば、能力の判定結果を投票で報告するというのも有りだと思うのだけど、使われているのを見たことは無い。これは何故だろう?

(追記) C410村では靈能結果の報告を投票で行う案を提案してみました。

Tags: 人狼

λ. お昼ごはん

本日のツッコミ(全3件) [ツッコミを入れる]

ψ yuragi@c365Joachim [○日に占った人が白なら×さん、黒なら△さんに投票っていうのだよね？意見として出たのは見たことあるけど、実行されたの..]

ψ yuragi@c365Joachim [朗報。Ａ２５０村の二日目で決行されてたよ。]

ψ さかい@c365Jacob [白黒だけでなく、誰を占ったかを投票で報告するとか幾つかバリエーションは考えてました。でも、どれも奇手の類かなぁ。 ..]

2006-06-01

λ. Cleanの定関数と定グラフ

<URL:http://d.hatena.ne.jp/lethevert/20060601/p1> より。

Haskellはグラフ書き換えによる意味論を言語仕様に採用していないので、言語仕様上はCleanの定関数や定グラフのような概念は存在しない。というか、そもそもHaskellの言語仕様は実行メカニズムをほとんど規定していない。では実際の処理系ではどうかというと、例えばGHCでは(ある種の最適化後に)ラムダ抽象以外の形をしている定義は、すべてCleanでいうところの定グラフとしてコンパイルされる。

full laziness transformation

また、full laziness transformation (full laziness optimisation, let-floating) によって、局所的な定義が大域的な定義に引き上げられることがあるので、大域的か局所的かの区別も存在しない。この full laziness transformation は大概は有用なのだが、時々困ったことをしてくれることもある。たとえば、以下のプログラムをコンパイルして実行するとメモリを食いつぶす。

f :: Int -> Int
f n = xs !! n
    where xs = [0..]

main :: IO ()
main =
    do print (f maxBound)
       print (f 0)

何故なら、full laziness transformation によって xs がトップレベルに引き上げられ、以下のようなプログラムと等しくなるため。結果、fが生きている限りxsも生きていることになり、メモリを食いつぶしてしまう。なお、「print (f 0)」を削除するとfがGCされxsもGCされるので、メモリを食いつぶすことはない(GHCではCleanと異なりCAFもGC対象になる)。

f :: Int -> Int
f n = xs !! n

xs :: [Int]  
xs = [0..]

main :: IO ()
main =
    do print (f maxBound)
       print (f 0)

では、こういうときにはどうするかというと、「-fno-full-laziness」というオプションを使って full laziness transformation を抑制してやる。全くしょーもないバッドノウハウである。

……とはいえ、Haskellはグラフ書き換え系を意味論として採用しておらず、おそらく今後とも採用しないことを考えると、言語自体による対応ではなくオプションやプラグマによって対応するというのは妥当なところだろう。個人的にはグローバルなオプションではなく、個々の定義に対して full laziness transformation を抑制するためのプラグマを付けられると良いと思うのだが……。