日々の流転

λ. 夢

水上/水中の奇抜なショーを見た。いろいろな演目があったけど、球体状に組まれたフレームに人が入って機械で水中から10メートルくらい打ち上げるやつが面白かった。打ち上げられて落ちてくるときの動きが、空中で何度か停止したりとか異様な動きをしながら落ちてきて面白かった。フレームのイルミネーションが残す残像も綺麗だった。

夢の中の僕には兄がいて、その兄にはIさんという彼女がいるのだけど、そのIさんと友だちも何人か来ていて、なかなか楽しそうだった。

それから、何日かして同じメンバで同じショーを見に行ったんだけど、今度は演技中に突然サメが現われて、逃げ遅れた演技者が一人頭からガブリとやられてしまった。

λ. 徐庶の微妙な冒険

爆笑。

ぱぱんだ日記(2002-02-27)より

λ. bof

なんか、久しぶりにブレスオブファイアの曲が聴きたくなってgoogle検索してみたら、MIDIファイルが幾つか見つかった。聴いてみると結構懐かしい。

λ. 東方紅魔郷

ノーマル、針。相変わらず進歩がないなぁ。th6_04.rpy

ノーマルクリア時点で2億点なんて普通にプレイしてて出来るもんなんですかね?

λ. UNION/FIND

今読んでいるwambookにUNION/FINDに基づいたユニフィケーションのアルゴリズムが載っていたのだけど、あまりに簡単で拍子抜け。これなら私も書いたことがあるや。ところで、UNION/FINDの計算量は almost linear すなわちアッカーマン関数の逆関数のオーダだとよく言われるけど、これってどうやって計算するのだろう?

λ. tDiaryを1.5.6にあげようと思ったのだけど、pstoreio.rbでエラーになったので、あっさり諦める。やっぱり2.0が出るのを待とうっと。

λ. Re: ObjectPool by さかいさん

えぇと、単に必要があったから書き換えただけで、継続的にメンテナンスする意思はないです。オブジェクトのプールはそれほど興味のあるテーマでもないので。

λ. 萌える弾幕STG もえだん

「萌える弾幕STG・もえだん」は、２次元弾幕少女（紅月ふらん・495歳）が弾幕勉強をナビゲートしてくれる 従来にはなかった新しい弾幕学習ゲームです。

「乙UN君」ってのに笑ったYO。萌へ萌へ日記(違)2004/03/01(月) より。

λ. Re: GNU Parted

わざわざParted専用のブートディスクを作らなくても、Knoppix辺りのCDにはPartedも入っていたと思うので、これを使ってしまうのが便利です。

λ. Representations of First order function types as terminal coalgebras, Thorsten Altenkirch

たまたま見かけて読んだのだけど、面白かった。α→βという関数型は、αが帰納的(inductive)な型であれば、余帰納的(coinductive)な型として表現できるという話。自然数やリストの場合までは考えたことがあったが、2分木のような線形でない型の場合も nested datatypes を使えば表現出来るというのは気づかなかったなぁ。

例:

自然数

(μX.1+X)→B ≅ νX.B×X

Aのリスト

(μX.1+A×X)→B ≅ νX.B×(A→X)

Aの2分木

(μX.A+X×X)→B ≅ (νF.ΛX.(A→X)×F(F(X)))(B)

証明は、ちょっと良く理解出来ていない所もある。セッティングは bicartesian で ω^op-limit と ω-colimit が存在する圏(cartesian-closedである必要はない)。そのままでは構成的関数からなる ω-Set のような圏へ一般化することは出来ないらしい……

関連エントリ

• [agda] ストリームの表現

λ. 米環境団体、捕鯨船妨害　薬品投げ込まれ３人けが

こういうのは「環境団体」ではなく「海賊」か「テロリスト」と呼ぶのが適切ではなかろうか。