日々の流転

λ. 今日も夕方まで寝てた。夢は覚えてない。

λ. イエス様は、数学の大定理でも証明しておいてくれれば良かったのだ。そしたら、きっと誰もがキリスト教を信じるだろうに。(笑)

λ. pの意味

あ、なるほど。状況依存セレクタを使えば良いのか。

ちょっと補足すると、元の文が書き変わってしまっているので意味が通じにくくなってしまったけど、「pが段落として使われているかといえば、必ずしもそうではないわけで…」というような事が書かれていて、なるほど確かにカレンダーやナビゲーションバーは意味的には「段落」じゃないよなぁと思ったわけです。今、元の文を読み返すと、そこで意図されていたのは、僕が読み取ったのと全く別の話だったようで、お恥ずかしい。

λ. 読書

『天国に涙はいらない 2 - 畜生道五十三次』

佐藤ケイ[著] さがのあおい[イラスト]

悪魔っ娘の次は猫耳娘っすか……

λ. 半構造データとは?

メモメモ。

中村さんの日記より

λ. 夕方に起きて朝方に眠る、ちょー駄目な生活中。

λ. 時符Extra8億

気分転換に妖々夢をやっていたら、時符Extraで8億を超えることに成功(th7_udsa03.rpy)。860993960点。あんまし粘らなかったのでカスリはいつもよりもだいぶ低いのだけど、残機ボーナスは大きいな。最後の3枚のスペルカードを落とさなければ9億いったかもよ(負け惜しみ)。でも、とりあえずExtraは目標の点数を達成したのでしばらくやんないけど。

λ. Re: ブロック

現在のRubyはブロックの種類による最適化は特にやってなくて、ブロックからはローカル変数を自由に触れます。ローカル変数の領域は最初はスタック上にallocaで確保されますが、そのスコープでProcオブジェクトが作られるとフラグが立ち、スコープから抜ける際にローカル変数の領域はヒープに移されます。

YARVは、ver.0.0.0cのソースやYARV アーキテクチャの妄想(Wed Jan 14 18:30:05 2004)を見る限りでは、この辺りはまだ実装されていないと思います。

λ. 二重黒死蝶ゲット

ついでに魍魎「二重黒死蝶」を回収。これで133/141。残るは、

• 蒼符「博愛のオルレアン人形」
• 獄炎剣「業風閃影陣」
• 獄神剣「業風神閃斬」
• 修羅剣「現世妄執 - Lunatic -」
• 人神剣「俗諦常住」
• 「人間と妖怪の境界」
• 結界「生と死の境界」
• 紫奥義「弾幕結界」

λ. Chu空間 (Chu Spaces)

先日、HDDを整理していたらhttp://chu.stanford.edu/を訳しかけたものが出てきたので、一応最後まで訳してhttp://web.sfc.keio.ac.jp/~sakai/doc/chu.stanford.edu/にこっそり置いておく(ただし品質については期待しないこと)。

Chu Space はなかなかに便利なフレームワークなので、もう少し広まってもいいんじゃないかと思う。

λ. Alloyで知識論理を使って論理パズルを解く

bonotakeさんの日記で時々取り上げられているAlloy、パズルを解くのに便利とのことなので、ちょっと週末に遊んでみた。 対象とするのは、以前にSPASSで知識の論理を使って論理パズルを解く?でも取りあげた「赤いぼうし」の問題で、これは以下のような問題。

AさんとBさんがいて、少なくとも一人は赤い帽子を被っていて、赤い帽子を被っていない人は白い帽子を被っている。ただし、二人とも他人の帽子の色は分かるが、自分の被っている帽子の色は分からない。そして、Aさんが「自分の帽子の色が分からない」と発言した。このとき、Bさんの被っている帽子の色は何か?　そして、Bさんは自分の被っている帽子の色が分かるか?

この前提となる状況をAlloyでは以下のようにモデル化することが出来る。

-- 世界
sig W {
   K_a: set W, -- 「Aさんが知っている」という様相の到達可能性関係
   K_b: set W, -- 「Bさんが知っている」という様相の到達可能性関係
}

-- 命題: 世界の集合を外延として持つ。
abstract sig Prop { ext: set W }

-- Aさんが赤い帽子を被っているという命題
one sig A_wears_a_redhat extends Prop { }

-- Bさんが赤い帽子を被っているという命題
one sig B_wears_a_redhat extends Prop { }

-- 公理
fact {
   -- K_aは同値関係(K_aはS5様相)
   all w1 : W | all w2 : W {
      (w2 in w1.*K_a or w1 in w2.K_a) implies w2 in w1.K_a
   }

   -- K_bは同値関係(K_bはS5様相)
   all w1 : W | all w2 : W {
      (w2 in w1.*K_b or w1 in w2.K_b) implies w2 in w1.K_b
   }

   all w : W {
      -- どちらかの帽子は赤である
      (w in A_wears_a_redhat.ext or w in B_wears_a_redhat.ext)

      -- AさんはBさんの帽子の色を知っている
      (all w1 : w.K_a | w1 in B_wears_a_redhat.ext) or
      (all w1 : w.K_a | not (w1 in B_wears_a_redhat.ext))

      -- BさんはAさんの帽子の色を知っている
      (all w1 : w.K_b | w1 in A_wears_a_redhat.ext) or
      (all w1 : w.K_b | not (w1 in A_wears_a_redhat.ext))

      -- Aさんは自分の帽子の色が分からない
      not (all w1 : w.K_a | w1 in A_wears_a_redhat.ext)
      not (all w1 : w.K_a | not (w1 in A_wears_a_redhat.ext))
   }

   -- 世界は一つ以上存在
   #W > 0
}

で、まずモデルが存在すること(無矛盾であること)を Alloy Analyzer でチェックする。

pred show() { }
run show for 10 W

これを実行すると以下のような結果とモデルが得られる。

Executing "Run show for 10 W"
   Solver=sat4j Bitwidth=4 MaxSeq=4 Symmetry=20
   11845 vars. 230 primary vars. 21671 clauses. 133ms.
Instance found. Predicate is consistent. 29ms.

B_wears_a_redhatが成り立っている世界があるので、Bさんの帽子がちゃんと決まるとしたら、それは赤の帽子。 なので、assertとcheckを使って反例がないかをチェックする。

assert test1 {
   all w : W | w in B_wears_a_redhat.ext
}
check test1 for 10

Executing "Check test1 for 10"
   Solver=sat4j Bitwidth=4 MaxSeq=7 Symmetry=20
   11935 vars. 240 primary vars. 21825 clauses. 150ms.
   No counterexample found. Assertion may be valid. 19ms.

結果、反例は見つからなかった。 もちろん、より大きなモデルに反例がある可能性はあるけど、まあこの場合には多分大丈夫だろう。

次に、Bさんが「自分は赤い帽子を被っている」ことを知っているかもチェック。

assert test2 {
   all w : W | all w1 : w.K_b | w1 in B_wears_a_redhat.ext
}
check test2 for 10

Executing "Check test2 for 10"
   Solver=sat4j Bitwidth=4 MaxSeq=7 Symmetry=20
   12123 vars. 250 primary vars. 22166 clauses. 133ms.
   No counterexample found. Assertion may be valid. 30ms.

やはり反例は見つからない。

というわけで、どうやらBさんの被っているのは赤い帽子で、しかもBさんもそのことを知っているようです。

参考

• The Alloy Analyzer
• Alloy関連ドキュメント (masateruさんのmixi日記より)
• 正しい仕様のみつけ方 —Alloy—
• [Alloy] - たけをの日記＠天竺から帰ってきたよ

λ. 冬景色

冬らしい寒々とした風景をもう少し味わいたかったが、昨日の雪はもうあらかた解けてしまって残念。

λ. 最終発表会打ち上げ

萩野・服部研の最終発表会後の打ち上げに参加。 OB比率高いよ……

λ. Ready for testing: Unicode support for Handle I/O

後で書く。