2002-11-05
λ. 比重
バス通りにある中学が校舎の建て替えをしている。現在は基礎を作っているようだ。まだコンクリートは流し込まれていない。そのうちコンクリートが流し込まれる時には死体でも投げ込んでみようか、等と思った。しかし、人間よりもコンクリの方が重そうだよなぁ。沈まないで浮いてしまわないか?
λ. 雲?
随分細長い雲だなぁと思ったら、煙突から立ち上る白煙だった。そういえば秋晴れだ。気が付けば随分肌寒くなったし、木々の紅葉も目を楽しませてくれるし、すっかり秋だなぁ。
λ. Plan9
またCDから起動して遊ぶ。DNSの設定をしようと/bin/ndb/local辺りのファイルを書き換えようかと思ったらリードオンリーだったので出来なかった。CDから起動しているのだからまあ当然か。
ramdiskかフロッピーか何かに書いてbindしてやればいいかとも考えたんだけど、考えてみれば名前空間はプロセス毎に独立なので意味が無いか。
ということはフォントの設定も出来ないのか。やっぱインストールしないとあまり楽しめなさそう。
λ. 召喚
夕食後に微睡んでいると召喚がかかる。萌ちゃんのためなら何処にでも行くさ!……なんちて。冗談。
λ. Haskell and XML: Generic Combinators or Type-Based Translation?
を読んだ。HaXMLカッコ良い!!
developerworksの記事よりもこっちの論文を読んだ方が分かりやすいな。
また、EDSLとコンビネータの例としても分かりやすかった。RDFを扱うEDSLを設計してみたくなった。
λ. 力学系の直観主義集合論
印刷した。力学系と言っても物理の話ではなくて、ダイナミック・システムの事。
2003-11-05
λ. ruby-ffcall
0.0.2をリリースしました。 今回の変更はruby-1.8対応などのマイナーな変更です。また、msvcrt用とcygwin用のバイナリパッケージも用意しました。
ruby-ffcallはruby-dlのDL.callbackを強化する拡張ライブラリです。DL.callbackでは使えるコールバック数に制限がありますが、FFCall.callbackにはそのような制限はありません。また、DL.callbackで作成したコールバック関数を開放するにはDL.remove_callbackを明示的に呼ぶ必要がありますが、FFCall.callbackではGCによって自動的に開放されます。
λ. 『ももいろさんご (5)』 花見沢 Q太郎
を読んだ。
λ. 教育方法の研究者が教育者として優れているとは限らない。
すごく同感です。あえて誰とは言わないけど……
λ. finite-set
% ruby -rfinite-set -e 'p (Set[true,false] == Set[true])' true
なんじゃこりゃ。……と思ったら速攻で原因発見。falseやnilを値として含み得る場合はEnumerable#findはEnumerable#any?の代用にはならないのか。考えてみれば当たり前だ。ついでに1.8でwarningが沢山出ていたのとかも含めてパッチ。
λ. 学校の帰り
駅前で民主党の候補が演説してた。たしか、今日は管直人と小沢一郎が来ると言ってたな。ちょっと見てみようかと思ったけど人多すぎ。そういえば今週末はもう選挙なんだよね。
λ. Relators, Fans and Membership
を見た。後ろの方はよく分からなかった。後で読み返さねば。
λ. Ruby-GNOME2のcygwin用パッケージ
これまでのパッケージはcygwin-ruby18.dllではなくcygruby18.dllをリンクしていたため、リリース版のRubyで利用できないと問題がありました。なので、パッケージを作り直しました。これでリリース版のRubyでも動作するようになるはずです。
λ. 論文積読
積読しまくり。
2004-11-05
λ. Super Mario Hopscotch
ラブ・ファミコン より。ちとはまってしまった。2つ目のステージのパーフェクトを取るのが難しかった。
λ. A206 峠の村
4日目にヤコブが人狼COしてオットーを狂人と言ったのだが、これは変だなぁと思った。仮にオットーが狂人なら、オットーがカタリナに人間判定を出した理由が理解出来ないのだ。狂人オットーはヤコブが最後の人狼だと知っていることになるので、ヤコブが人狼確定してしまうカタリナ人間判定よりも、ヤコブが人狼確定せずに済むカタリナ人狼判定を出すべきだからだ。
| ニコラス (占い師CO,襲撃された) | ヤコブ (占い師CO) | ジムゾン (村人CO,処刑された) | オットー (霊能者CO) | カタリナ (霊能者CO,処刑された) | オットーの カタリナ人間判定 | オットーの カタリナ人狼判定 |
|---|---|---|---|---|---|---|
| 占い師 | 人狼 | 人狼 | 霊能者 | 狂人 | ○ | |
| 占い師 | 人狼 | 人狼 | 狂人 | 人狼 | ○ | ○ |
| 占い師 | 狂人 | 人狼 | 霊能者 | 人狼 | ○ | |
| 占い師 | 人狼 | 人狼 | 霊能者 | 人狼 | ○ | |
| 狂人 | 占い師 | 人狼 | 霊能者 | 人狼 | ○ | |
| 狂人 | 人狼 | ？ | 人狼 | 霊能者 | ○ | ○ |
| 狂人 | 人狼 | 人間 | 人狼 | 人狼 | ○ | ○ |
λ. (β→γ)→(α→β)→α→γ
First Steps in Modal Logic について雑談してるときに「(β→γ)→(α→β)→α→γ」をヒルベルト流(ただし論理公理は (s) (α→β→γ)→(α→β)→α→γ と (k) α→β→α のみ)でとっさに証明できなくてちょっと悔しかった。λ式で書くなら λf.λg.λx. f (g x) でおしまいだし、自然演繹やシーケント計算でもそれは同じだけど、ヒルベルト流だとすぐには思いつかんよ。
後でこのλ式をSKIコンビネータの式に機械的に変換してみると「S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(KI))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(KK)(KI))))))(S(S(KS)(S(KK)(KK)))(S(KK)(KI))))」になった。もっと短く出来そうではあるけど、流石にこれは思いつけないよなぁ……
というか、アレだ。演繹定理(Deduction Theorem, 「Γ,α⊢β ⇔ Γ⊢α→β」)を使ってしまえば良かったのか。そりゃそうだ。
2007-11-05 Елена Исинбаева たん、はぁはぁ
λ. 型システムを設計する方法論
Type Systems for Resource Bounded Programming and Compilation - Case for Support よりメモ。
The methodology for achieving these goals will be as before: analyse the common patterns of representative case studies, identify appropriate invariants, cast them into an abstract (usually category-theoretic) model, and finally describe the model by a type system.
2008-11-05
λ. ロシアンマスターズ！EX
というのを紹介された。 元ネタはわかんないけど凄いなぁ。
λ. 水泳
今日も1km泳いできた。 気のせいかも知れないけど、なんだか水温が少し上がっていた気がする。
λ. Election Results 2008
オバマ候補の大勝か。素晴らしい事だとは思うけど素直に喜べない自分がいる。ブッシュ政権はアレだったかも知れないけど、一方でその前のクリントン政権がどうだったかを思い出すと、ね。
2009-11-05
λ. iPhone で使うGoogle Reader のクライアントを RSS Flash g free から rss に乗り換えた
RSS Flash g free が起動しなくなったので、こないだ無料だったrssに乗り替えた。 UIはrssの方がiPhoneの標準的な感じだなぁ。 未読に戻す昨日が無いのは少し不満だけど、概ね満足。 これまで Feeds ⇒ RSS Flash g free ⇒ rss と乗り替えてきたが、Google Reader のクライアントひとつで、これだけ選択肢のあるiPhoneは……
