日々の流転

λ. 明日から学校なので、床屋行って来た。

λ. う、最近、Rubyネタが無いぞ。Ruby Hotlinksに登録されているのに、申し訳ないなぁ。とりあえず、Gimp-Rubyのsetup.rbを新しいやつにでも入れ換えるか…

λ. 読んだ本

『ギルティギア ゼクス - 白銀の疾雷』

海法紀光[原作]　石渡大輔[イラスト]

ブレンパワード 1

ブレンパワード 2

杉崎ゆきる[漫画] 富野由悠季[原作]

λ. 時間割りを貰いに学校へ。

λ. 1996年以前のbitは配架が白楽で、"コンピュータによるモンゴル語文字処理の現状"はコピーできなかった。取り寄せるのはまた今度にしよう。

λ. はぁ、「君が望む永遠」ですか……

λ. 買った本

『黒猫の三角』

皇なつき[漫画] 森博嗣[原作]

『封建主義者かく語りき』

呉智英[著]

『構造改革論の誤解』

野口旭, 田中秀臣 [著]

λ. 読書

『夢使い』3

植芝 理一

λ. 人狼BBS 57 谷底の村

人狼BBS初参加で、ここ一週間ほどこの「谷底の村」に参加してました。この一週間は長いようで本当に短かったです。この感動をどう表現したらよいか分らないし、もうこの村では一緒に参加した他のプレーヤーと話すことが出来ないことを思うと、名残惜しくてたまりません。このゲームを生み出したにんじんさん、そして何よりも一緒に参加した全てのプレーヤーに心から感謝します。

心残りの一つは、最後のリーザさん(パントさん)のセリフに対して、「……ッ！！　くッくくッ　上等じゃないか　女！！　上等ぉ！！」と返す事が出来なかったことです。別のネタを考えていたせいで、とっさに反応できなかったんです。「画竜点睛を欠く」とはまさにこういうことを言うんでしょうね。本当に悔しいなぁ。

• 人狼BBS まとめサイト - 57村
• 人狼BBS まとめサイト - msakai

λ. 『迷宮百年の睡魔』, 森 博嗣 [著]

読了。森博嗣の作品の中ではこのシリーズ(?)が一番好きかも。それと、読んでるあいだ頭に浮かぶ情景は全部スズキ ユカの絵でした。『女王の百年密室』に続いてこれもスズキ ユカの絵で漫画化されないかなぁ。

λ. An Implementation of a setoid model in Agda

Extensional Equality in Intensional Type Theory の setoid model を、LEGOでの実装を元にAgdaで実装中。大体実装できた。

(2005-09-30 追記) だいぶ苦戦してしまったが、基本的な部分を何とか書けた。色々汚いので、きれいに書き直したいな。それと、LEGOでの実装と比較しなくては。

Meta.agda

Approximative Implementation of the meta theory.

Setoid.agda

Definition of the core model.

Compr.agda

Definition of context comprehension.

Pi.agda

Definition of ∏-types.

Prod.agda

Definition of (non-dependent) product types.

Id.agda

Definition of Identity types.

λ. 旅行

λ. 『ガセネッタ＆(と)シモネッタ』 米原 万里

を読んだ。

λ. 正格な言語での不動点演算子

正格な言語、例えばOCamlでは、以下のようにして不動点演算子を定義することが出来る*1。これは常識ですね。

# let rec fix f x = f (fix f) x ;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let fib' f x = if x <= 1 then 1 else f (x - 1) + f (x - 2) ;;
val fib' : (int -> int) -> int -> int = <fun>
# let fib = fix fib' ;;
val fib : int -> int = <fun>
# fib 10 ;;
- : int = 89

で、ここでクイズなのだけど、f に対して fix f というのは一体何者でしょうか?　「そんなの f の最小不動点に決まってるじゃん」と思うかも知れないけど、ここでは正格な言語を考えているので「f ⊥ = ⊥」で、最小不動点は⊥なのでした。

λ. 家計簿探し

社会人になってお金の出入りも増え、入出力をきちんと記録した方が良いと思うようになったので、何か良い家計簿ソフトはないかと探している。 とりあえず以下のような点に注目して探している*1けど、なかなか良いのはないね。

• Webベースか?
• メールで登録可能か?
• 複式か?

λ. foonance.com

最初に試したのがこのfoonance.comだけど、使い物にならない。 概念はシンプルそうで良いけど、色々とバグってるっぽい。

また、日本語をちゃんと使えない。Money Stores で Short name に日本語を使うと化けるうえに、transation を正常に追加できない。Description の方は平気。Category や Budget にも日本語は使えない(?)。Currency Symbol には円記号(YEN SIGN, U+00A5)を指定しても大丈夫だった(ただし、互換領域の FULLWIDTH YEN SIGN (U+FFE5) だと化けるっぽい)。

それから、一度作成した Money Store や Transaction は削除は出来ても編集出来ない。

λ. シンプル家計簿

特徴をみると魅力的なんだけど、登録の時にミスったようで重複した勘定項目が出来てしまい、削除しようとしたら例外が発生。 後でまた試す。

λ. GnuCache

Windows版をインストールしたが、gconfdがエラーで正しく起動しない。 これはWebベースではないけど、<URL:http://members.jcom.home.ne.jp/tanitsu/2006-10-21.html#2006-10-21-2> の記述を見る限り使いやすそうだったので残念。

λ. Wasabe.com

.