日々の流転

λ. AVL木

暇潰しにAVL木のコードを書いて、バグってたのでムッキー。

[2005-04-19 追記] 不変量を型によって強制することによって、ここで犯したようなミスはほとんど回避できる。詳しくは、AVL木でGADTを試してみる を見よ。

λ. Y^T×S ≅ (Y^T)^S の証明についてのメモ

map object と evaluation map を以下のようにおく。

• e₁: (T×S)×Y^T×S→Y
• e₂: S×(Y^T)^S→Y^T
• e₃: T×Y^T→Y

e₁ は T×X→Y の形なので、e₃について
e₁ = e₃(1_T×[e₁]) ……(1)

ここで、[e₁]: S×Y^T×S→Y^T は、S×X→Y^T の形なので、e₂について、
[e₁] = e₂(1_S×[[e₁]]) ……(2)
1_T×[e₁] = (1_T×e₂) (1_T×S×[[e₁]]) ……(2')

ところで、e₃(1_T×e₂): T×S×(Y^T)^S→Y は (T×S)×X→Yの形をしているので、e₁について、
e₃(1_T×e₂) = e₁(1_T×S×[e₃(1_T×e₂)]) ……(3)

e₁(1_T×S×[e₃(1_T×e₂)] [[e₁]])
= e₁(1_T×S×[e₃(1_T×e₂)]) (1_T×S×[[e₁]])
= e₃(1_T×e₂) (1_T×S×[[e₁]]) (∵(3))
= e₃(1_T×[e₁]) (∵(2'))
= e₁ (∵(1))

∴ e₁(1_T×S×[e₃(1_T×e₂)] [[e₁]]) = e₁ …(4)

e₃(1_T×e₂) (1_T×S×[[e₁]] [e₃(1_T×e₂)])
= e₃(1_T×e₂) (1_T×S×[[e₁]]) (1_T×S×[e₃(1_T×e₂)])
= e₃(1_T×[e₁]) (1_T×S×[e₃(1_T×e₂)]) (∵(2'))
= e₁(1_T×S×[e₃(1_T×e₂)]) (∵(1))
= e₃(1_T×e₂) (∵(3))

∴ e₃(1_T×e₂) (1_T×S×[[e₁]] [e₃(1_T×e₂)]) = e₃(1_T×e₂) …(5)

[2005-04-19 追記] Y^T×S ≅ (Y^T)^S は結局初等的な証明は出来るんだっけ?　米田の補題を使えば簡単に言えるけど。

【2008-06-08 追記】 単に米田の補題の証明を展開すればいいだけ。

λ. 借りた本

『数学パズル ものまね鳥をまねる—愉快なパズルと結合子論理の夢の鳥物語』

レイモンド・スマリヤン(Raymond Smullyan)[著], 阿部 剛久, 福島 修身, 黒沢 俊雄, 山口 裕 [訳]

λ. GNOME2

libIDLとORBit2のパッチをcommit。scanfが64bit整数を扱えない問題にはまだ対処していないので、libIDLをコンパイルする際には./configure.inを書き換えて誤魔化す必要があるでしょう。

λ. 『委員長お手をどうぞ』, 山名 沢湖

を読んだ。ほのぼのしてていいですな。4コマ委員長(4)の「おリボンは　いざというとき　しおりにもなって便利です」に笑った。

λ. ジンギスカンキャラメル

決して不味くはないのだけど、すごい違和感だなぁ。誰が持ってきたのか知らないけどGJ!

λ. The SLam Calculus: Programming with Secrecy and Integrity - Nevin Heintze and Jon G. Riecke

型システムを使ってデータの機密性を保障しようというのは誰でも考えるアイディアだけれど、実用的なシステムを作るのは結構難しいのね。この論文でまず面白いと思ったのは、direct reader と indirect reader を区別していて、両者への情報流に対して別の制約を与えられる点。

それから、Non-interference Theorem も面白い。論理関係をセキュリティに応用する話は Logical Relations for Encryption にもあったな。

• YuichiTanakaの日記 : SLam Calculus

λ. モーニング・ブルーズを解消する賢い目覚まし

睡眠中の脳波を測定して、睡眠パターンを割り出し、最も眠りが浅くなった時にアラームが鳴る賢い目覚まし時計が発明された。

やべぇ。ちょー欲しいんだけど。

λ. ドメイン認証の問題点と解決案

を読んだ。/.J の IPアドレスの最近傍識別を行うSPAM Filter より。

λ. RHG読書会::東京 入門JavaScript 第四回

先月はなかったので二ヶ月ぶり。 RHG読書会みたいな楽しさは久しぶりで、なんだか元気をもらった気がする。

jsthread

牧さんのjsthreadの話が面白かった。jsthreadはプリエンプティブなスレッドを実装したJavaScriptライブラリ。

• <URL:http://sourceforge.net/projects/jsthread/>
• <URL:http://jsthread.sourceforge.net/>

今回の話を聞くまでは「CPS変換して継続呼び出しをsetTimeoutを介するようにすれば良いだけじゃん」とか思っていたのだが、実際に話を聴いたら面白かった。

Function#toStringで取得した関数のソースコードをパースし Trampolined Style に変換する。そして、変換結果をその関数のプロパティに保存しておく。このライブラリは関数を呼ぶ際にこのプロパティが存在するかチェックし、存在しない場合には普通の関数呼び出しを行い、存在する場合にはそれをスケジューラに渡して呼び出す。 このようになっているために、変換されていないコードから変換済みの関数を呼び出す際にも問題が起こらないようになっている。 考えてみればJavaScriptらしい自然な設計ではあるが、細かいところまで良く出来ていると感じた。

本質的な問題は変換対象の関数が自由変数を含む場合。JavaScriptには環境を明示的に操作する機能はないと思うので、自由変数にアクセスできないはず。 ……と思ったが、Firefoxではevalの第二引数を使うことで以下のようにアクセスできた。IEやOperaではダメだったけど。

var f = (function(x){ return function(){ return x } })(10)
eval("x", f) //=> 10
eval("function(z){x=z}", f)(100)

ということは、Firefoxのことだけを考えるのなら jsthread-fv-firefox.diff のようにすれば良い。

それから、JavaScriptのパーサがソースコード中の大きな量を占めている。個人的に「JavaScriptでパーサはあまり書きたくないなぁ」と思っていたが……　なお、パーサはRhinoのコードを翻訳したそうで、拡張構文(?)もそのまま使えるそうだ。

あと、このような変換ではプログラムの意味が変わってしまうので、変換の正当性をどのように定義するかが難しいそうだ。

関連

• ライフ - L'eclat des jours(2007-04-15)
• JavaScript でプリエンプティブなスレッドを - val it : α → α = fun

λ. 日本Ruby会議2007のチケット

今日10:00に発売で13:30頃に売り切れだったとか。 買えなかった……しょぼーん。

というか、そもそも今日発売だったこと自体を知らなかった。 最近アンテナが低すぎな私 orz

そういえば、プログラムをみて気付いたのだが、今回はむとうさんも発表するのだな。むとうさんはあまりこういうイベントには出てこない印象があったので楽しみ。

λ. Mozyを使い始めた

オンラインバックアップサービス「Mozy」を使ってみた − ＠IT で紹介されていたオンラインバックアップサービスの Mozy を使い始めた。

詳しい説明は＠ITにあるけど、無料で2GBまで使えるというのは素晴らしいし、非常に手軽で便利。また、自宅の別ハードディスクにバックアップするのに比べて、オンラインバックアップサービスは地理的なリスクを分散出来て良さそうだ。 暗号化に用いる鍵はMozyの用意する鍵を使うことも出来るかが、念のため自分で鍵を用意して使うことにした*1。

ちなみに、紹介システムがあって、以下のリンクから Mozy のホームページに行って登録すると、登録者と紹介者(私)が二人とも256MBの容量を余分にもらえるみたい。

• <URL:https://mozy.com/?ref=ZKLCNC>

λ. GADTに対するexhaustiveなパターンマッチ

exhaustive な switch - まめめも で思い出したが、GADTに対してパターンマッチするとき、型による制約から実際にはexhaustiveなパターンマッチなのに、GHCがそれを認識してくれなくて悲しいことがある。 例えば、こんな感じのコードの場合。

data T a where
    Foo :: T Bool
    Bar :: T Int

f :: T Bool -> Int
f Foo = 0

これってGHCの実装が不十分なため?　 それとも本質的に判定不可能なものなのだろうか。

λ. iPhoneのカメラには接写機能が無いのね

iPhoneのカメラには接写機能が無いのね。 名刺の写真をとったりというのは難しそうだ。

iPhoneでとった写真:

二年前に買った携帯でとった写真: