日々の流転

λ. なんつーか、やる気なくてすんません。

λ. 麻生さん勇気あるなー

λ. 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で作った)を試してみた限りではすべてエラーになってしまったのだけど、将来に期待。

λ. インフレターゲットFAQリンク集

めも。黒木のなんでも掲示板２ (0055)より。

λ. ダブル・ジョパディ

を見た。

λ. 爪を切りたいのに爪切りが見つからない……

λ. 「♪しんのすけ日記♪」からRefererが飛んでくるのだけど、見てみるとリンクもないし、ちょっと気になる。

λ. リクナビに登録

とりあえず、リクナビ2005に登録してみる。就職活動開始!?

λ. バスタード・完全版第2巻発売記念スペシャルコーナー

というわけで、ようやく発売されたらしい。

λ. 木下佳樹, 高橋孝一: 『図式による圏論の形式的証明』, 電子技術総合研究所研究速報, TR95-25, 1995.

を簡単に読んだ。順当な方法だとは思うけど、これで項の表現を思い浮かべずに図形だけ見て証明できるかと言われれば、(僕の頭には)少し厳しいような気がする。そういえば、以前はアプレットを公開してたような気がするけど、もうアプレットの公開はやめっちゃったのかなぁ。だとしたらちょっと残念。

λ. Re: な、なんで受かっちゃうかな。。 (2003-06-04)

2003.6.4 な、なんで受かっちゃうかな。。
日曜日　東地区　“エ”ブロック　51a
「ブロンプトンvsトランジットコンパクト」（予定）。ジャンルは折り畳み自転車布教（何それ）。輪行啓蒙でも可。
初参加。コピー誌のつもりです。頑張ります。ちょっと（どころでなく）気合い入った。

おぉ。おめでとー。

λ. Hylomorphism その2

Shortcut Deforestation in Calculational Form によると、CPOでは initial algebra と final coalgebra のキャリアが一致してしまうらしい。逆極限法(inverse limit construction)については今勉強中なんで良く分からないのだけど、いまいちピンとこない。

[2005-06-04 追記] Haskellの代数的データ型は始代数ではない? を参照。

λ. Rubyユーザの喫煙率

私も煙草は吸いませんねぇ。子どものころ喘息だったこともあって、どうも苦手なんです。

λ. なにか

某氏に

• 萌え.jp 画像掲示版
• ふたば☆ちゃんねる

というサイトを教えてもらう。

λ. 横山哲郎, 『効果的な融合変換のための変換戦略の記述法とその実現』

を読んだ。

λ. String#intern

1.8では空文字列のinternはエラーになったのね。Rinnではまった。

λ. 夕食

豊田さんと中村さんと。しそラーメン。

λ. ようやく重い腰をあげて Canbe (PC-9821 Cu13) を片付けた。高校に入学した時に買ってもらったPCなので、もう6年になる。長い間ご苦労さま。これまで本当にありがとう。

λ. EAC

Windows用のCDのRipper。chicaに教えてもらう。

λ. チェーン・リアクション

を観た。

λ. 汚れたら洗える心

「汚れたら洗えるキーボード」(/.J)を見て、「汚れたら洗える心」と誤読。

λ. Nested Type

CPLに追加できないかと思い Nested Type についてちょっと調べる。とりあえず R. Bird の論文。

• Nested Datatypes
• Generalised folds for nested datatypes

λ. 水泳

平泳ぎ。なるほど、背筋と胸の筋肉をあんな風に使うのか。

λ. インターフェース設計論のレポートを書けなくて徹夜。文章が出て来ないのは辛いなぁ〜

λ. インターフェース設計論

レポートを何とかでっち上げる。もうどうでもいいや。で、遅れて教室に行ったら、増井さんが講演(「モバイル/ユビキタス時代のユーザインタフェース」)していて驚く。そうか、そういえばそんな予定だったんだ。それほど目新しい話はなかったけど、直接話を聴くのは初めてだったので楽しかったです。

λ. 萩野服部研

SICP。今日は「論理プログラミング」の章。

「ノットらん」は聞いてはいたのですが、眠くて反応できませんですた。

λ. Charity User Manual (draft)

を読んだ。ふむ、fold/unfold/mapだけでなくcase/recordをプリミティブに追加しているのか。それ以外は正直いまいちな気がする。

λ. 夢

「線形の理論」のSAでスーファミ版のマリオカートをする夢を見た。

λ. ドイツ語

9:25に教室に入ったら誰もいなくてちょっと焦る。

λ. 借りた本

『CORBA完全解説』

小野沢 博文 [著]

『分散オブジェクト指向 CORBA - 分散プログラミングから大規模分散システム構築まで』 (UNDERSTAINDING CORBA)

R・オッティ(Randy Otte), P・パトリック(Paul B. Patrick, Sr), M・ロイ(Mark Roy) [著], MISCOオブジェクト指向研究会 [訳], 満尾 晃一 [監修]

『社長失格 - ぼくの会社がつぶれた理由』

板倉 雄一郎 [著]

λ. Matrix Reloaded

rqlの人たちと見てきた。映像は結構楽しめた。ストーリィは……こーいうのが好きな人にはいいんじゃないですかね?

λ. Linear Logic

• Linear logic, by Patrick Lincoln.
• A Brief Guide to Linear Logic, by Andre Scedrov.

線形論理についてちょっと調べる。

λ. 今日の向井研

先週話すつもりだった、最小不動点に関するイントロダクションを話してみる。

λ. 夕食

片山さんとニューオリ。鶏肉のトマト煮スパゲティ。

λ. ファイト・クラブ

想像してたよりは良かった。が、「再会」した後のテイラーの、あの筋肉馬鹿っぽい描写が、すべてを台無しにしてると思う。

λ. Linear Logic

「λ計算のかわりに線形論理を使う」というのは、結局「計算 = 項の簡約 = 証明の正規化(カット除去)」というアイディアをそのまま線形論理で使うって事なのかな?

λ. スパイ・ゾルゲ

見てきた。とても良かったし、『日本人が忘れ去ろうとしている「昭和」　日本人が失いつつある「時代感覚」　日本と日本人が取り戻すべき「アイデンティティ」　その、まるごとを描いてみたかった』という目論見も成功しているように思う。最近見た映画の中では一番良かった。けど、3時間以上ってのはさすがに長すぎ。

【追記】しかし、いくらなんでも尾崎秀実を美化しすぎだろ。

λ. JRuby-0.5.3

ふと、JRubyを使えばcpl.rbを簡単にアプレット化出来るんじゃないかなぁとか思い、JRubyを試してみる。実装されていないクラスがあったり挙動が若干違うというのは覚悟してたのだけど、それ以外にも問題はあるみたい。例えば、異なるモジュールで定義された同名のクラスが区別されないとか。

module Foo
  class Parser
    def foo
      "foo"
    end
  end
end
 
module Bar
  class Parser
    def bar
      "bar"
    end
  end
end
 
p Foo::Parser #=> Foo::Parser
p Bar::Parser #=> Foo::Parser (!?)
 
p Foo::Parser.new.bar #=> "bar" (!?)
p Bar::Parser.new.foo #=> "foo" (!?)

λ. 『妻みぐい2 [ADULT]』

Amazonにこんなのを勧められる。お勧めの理由(の一つ)は『計算機プログラムの構造と解釈』を評価してたかららしい。ビバSICP。

λ. ALGI-13 Proceedings

数理解析研究所講究録１３１８
短期共同研究 代数・論理・幾何と情報科学
京都大学数理解析研究所
２００３年５月刊

λ. ドイツ語

藁谷先生は面白いなぁ。

λ. 萩野服部研

SICP 5.1 「レジスタ計算機の設計」

λ. [a₁; a₂...; a_n] と[b₁; b₂...; b_n] を受け取って, [(a₁, b_n); (a₂, b_{n - 1}); ...; (a_n, b₁)] を返す関数

水凪さんの日記の4/17に載っていた問題。帰りの電車とバスの中で結構真剣に考えてしまった。気づけば簡単。

長さの等しい二つのリスト[a₁; a₂...; a_n]と [b₁; b₂...; b_n]を 受け取って, [(a₁, b_n); (a₂, b_{n - 1}); ...; (a_n, b₁)] を返す関数を書きなさい。 ただし、

• nをあらかじめ知ることはできない
• 与えられた二つのリスト以外のリストを使ってはならない
• 再帰呼び出しは高々(n + 1)回しか行ってはならない
• 全体の計算量はO(n)でなければならない

λ. 昼食

久しぶりに看護の方の食堂へ。

λ. cpl.rb

cpl.rbをJRubyで動くようにし、それからSwingで簡単なUIをつけてみた。後はアプレット化するだけなのだけど、jarに同梱したスクリプトをrequireする方法がよくわからない。

rear.rbで一つのファイルにまとめておいてevalするとか考えたのだけど、JRubyにbindingが実装されてなくて動かなかったので諦める。うーむ、やっぱJRubyに手を入れなくちゃダメかなぁ。。

λ. 借りた本

『CORBA完全解説 - POAを使いこなす』

小野沢 博文 [著]

λ. 夕食

豊田さんと水龍。

λ. A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points

を読んだ。Lawvere's diagonal theorem を使っていろんなパラドクスや不動点定理を整理している。面白い。

λ. 夢

某チャッピー氏に「痛い日記、禁止!」と言われる夢をみた。

λ. Linear Types Can Change the World!

を読んだ。

λ. 夕食

片山さんとデニーズ。バンコクガイパッごはんプレート。「ガイパッ」ってどういう意味なのかなぁ。

λ. RSS/RDF

「FeedReader(?)で読めねぇぞ、ゴルァ」と言われたので、生成しているRSSをeuc-jpからutf-8にしてみる。ついでに、自分でもSharp Readerという RSS Aggregator を使い始める。ほほぅ、こいつはなかなか便利。

λ. ウォーター・ボーイズ

面白すぎ。

λ. やる気が急速にダウン中。色々ごめんなさい。

λ. 水泳

前の時間のドイツ語が早く終わったので、ご飯を食べてから水泳の授業へ。が、これは大失敗。気持ち悪ぅ。うぇっぷ。……というのはサテオキ、私って背泳ぎダメダメだ。

λ. Final Coalgebras are Ideal Completions of Initial Algebras

メモ。

λ. Re: む、次は痛い日記禁止キャンペーソですか。(事実誤認)

ガガーソ。禁止第一号はやっぱこの日記ですかね? 困ったなぁ (^^;;

λ. Config::PkgConfig:

pkg-config の Perl interface らしい。(The diary formerly known as Go ahead make my day. (2003-06-20)より)

Ruby-GNOME2でもextconf.rbのコードの共通化のために簡単なインターフェースを用意してるのだけど、独立した形にしておいた方が良い?

λ. texdiary

「TeX の数式や文書を画像に変換して貼り込む tDiary プラグイン」。おぉ、便利そうだ。web.sfc.keio.ac.jpにTeX関係がインストールされていないのが残念。

λ. 地下室?　地下鉄?

久野君が「地下室」と言おうとして「地下鉄」と言い間違えまくる。おーい、君はいつから「鉄」になってんだー

λ. 借りた本

『ユーザーイリュージョン - 意識という幻想』

トール・ノーレットランダーシュ(Tor Nørretranders)[著] 柴田 裕之 [訳]

『計算論 - 計算可能性とラムダ計算』

高橋 正子 [著]

『線型論理入門』

竹内 外史 [著]

『キノの旅Ⅶ - the Beautiful World』

時雨沢 恵一 [著] 黒星 紅白 [イラスト]

『LUNO (1)』

冬目 景 [著]

λ. 『夢使い (4)』　植芝 理一

を読んだ。

λ. 人妻コスプレ喫茶 [アダルト]

Amazonにこんなのを勧められる。「おすすめ理由」はベルセルクを買っていたかららしい。先日の「妻みぐい2」といい、何と言うか(以下略)

λ. FOAF

研究室で30分くらいはやったので、私も自分のFOAFを作ってみました。後でFOAFのデータを使って遊べないか考えてみよう。

λ. 空色勾玉

有野さんが薦めているようなので、ウィッシュリストに追加。

λ. 超循環

超循環(メタサーキュレーション)。

λ. 眠い。

λ. D_∞わからーん

D_∞わからーん。逆極限法(inverse limit construction)わからーん。

λ. 線形の理論

「アイを知らずに一生を終える人が増えるんだねぇ」

高校数学から復複素数がなくなるとかいう話をしていて、田中先生が一言。

λ. Lambek's Lemma

始代数(initial algebra)と終余代数(final coalgebra)の構造射が同型射である事はかなり簡単に証明できるのだけど、これには Lambek's Lemma という大層な名前がついているらしい。

【2006-01-18 追記】 オリジナルは J. Lambek, Subequalizers, Canad. Math. Bull. 13 (1970) 337-349. らしい。

λ. ビリヤード

中村さんと豊田さんに連れられてビリヤードをやった。ビリヤードがこんなに面白いものだとは知らなかった。それにしても、二人ともうまいなぁ。

λ. 夕食

豊田さんとサイゼリア。
ルーコラときのこのピザ, パルマ風スパゲティ

λ. Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors

メモ。

【2006-07-23追記】 久しぶりに読んだらだいぶイメージがわくようになっていた。まだきちんと追いかけることは出来ないけど。

λ. taiikukai

秩父宮体育館でバスケ。バスケなんてやるの何年ぶりだろう。ルールもすっかり忘れてて焦る。スリーポイントシュートって何だっけ? みたいな。4分程度のミニゲームを何度かやったのだけど、4分って長いね……。ダメじゃん、俺。でも、何故か運動量が多いと思われてしまい、不思議なのだ。

関係ないけど、「姪御さん」が「メイドさん」に聞こえてしまってビックリする。久野君の影響か。

λ. 夕食

taiikukaiメンバに中村さんを加えて、藤沢のハンバーグ屋さん(?)のGruppeへ。GruppeはJパスタの下のお店で、なかなか美味しかった。
ヘルシーチキンハンバーグ

λ. スマッシュブラザーズ大会

それから帰る途中でチカと唯から召喚され、大乱闘スマッシュブラザーズDX大会に突入。それから、ビューティフル ジョー というゲームをみしてもらう。ほほぅ。最近のCAPCOMはこんなゲームを出しているのか。

帰って風呂に入ったら、もう午前4時。寝なきゃ……

λ. 軽い筋肉痛

λ. 湘南高校の文化祭に行こうかと思ってたのだけど、なんか面倒になってしまって、結局行かなかった。

λ. 「自己言及の論理と計算」 (長谷川 真人)

対角線論法と不動点に関するチュートリアル。逆極限法(inverse limit construction)についても取り上げてる。ちなみに、逆極限法によって領域方程式 D ≅ [D→D] の解を求める方法については 「再帰データ領域 Ｄ∞モデル」 も参照すると良いと思う。

ところで、少し前に「A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points」という論文を読んだ事を思い出して、関連論文をAmazon風に紹介をしてくれるサイトがあったらどうかなぁとか少し思った。例えば、

あわせて読みたい

「自己言及の論理と計算」と「A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points」、どちらもおすすめ！
ページ数合計: 44ページ

とか。

[2005-03-27 追記] この論文については haskell-jpメーリングリスト で結構長いスレッドが出来ている。

• [haskell-jp:216] 不動点としての再帰プログラム
• [haskell-jp:297] Xn 問題
• [haskell-jp:317] X(n) <-> X(n+1) 問題

あと、[haskell-jp:227] で data X = PsiInv (X -> (Int -> Int)) と書きましたけど、これは data ではなく newtype にすべきでしたね。

λ. 夕食

太太でジャージャー麺と餃子。

λ. ゲームプログラミング

の最終課題に向けてちょっといじり出す。不動浮動小数点数を使えないのは不便だなぁ。仕方ないので固定小数点数で扱う事に。で、てきとーに、sin(), cos() はテーブルで実装して、sqrt()もてきとーにニュートン法で計算する事にしよう。けど、atan()ってどうやって実装するのが普通なんだろ? って所で中断。 ぐぐってみると、CORDIC法というのがあるようだ。

λ. お昼

富山名物、ます寿司。

λ. 水泳

水中カメラで自分の泳ぎを観察する予定だったので楽しみにしていたのだけど、水中カメラの調子が悪かったとかで、かわりにクロールのコツについて教わった。

• サムエントリー
• ハイエルボー
• S字プル
• 手をいれるタイミングとキックのタイミングを合わせる (そのためにツーキックの練習をしたのだけどムズかった)
• (もう一つ教わったはずだけど、思い出せない。ローリングに関することだったかも。)

λ. Teach Yourself Scheme in Fixnum Days

LISP Scheme Part7 (772)より。Fixnum days ってあんた…… (笑)