日々の流転

λ. 研究会最終発表

その後打ち上げ。昨年に続いて某氏の誕生日を祝う。

λ. 風俗嬢の末路

あろはさんのmixi日記より。最初テキストを読んだときはあまり感じるものはなかったんだが、写真を見てショックを受け、テキストを読み返したら本当にいたたまれなくなった。なんというか……言葉が見つからない。

他人事と思い、汚らしいと蔑む人や、自業自得と言う人もいるけれど、それは少し違うんじゃないかと思う。人類の歴史を見れば太古の昔から売春はあり、売春の存在しなかった文明などまずないだろうし、これからも売春が無くなるとは考えにくい。善悪はともかく、売春というのは現在の社会や文明のシステムの一部と言ってよい。そして私もこれを読んでいるアナタもこの社会に生まれこの社会に依存して生きている。自分が直接関わっていないからといって、蔑み悪意を投げつける気にはなれない。

どのような経緯で彼女が風俗嬢になったのかは分からないが、彼女に救いがあることを心から願う。

λ. MAD PEOPLE 用の発言フィルタ

• madpeople-message-filter.user.js

例によってGreasemonkeyを利用した発言フィルタを作った。 Greasemonkeyをインストールし、上のファイルを右クリックし「Install User Script」を選択すればインストール出来る。使い方は MAD PEOPLE のエピソードを表示してみればわかると思う。

【追記】 スナッチによって生者で死者で同じ顔の人がいる場合、区別するようにしたほうが良いのかな?

【8/17追記】 本体に発言フィルタが追加されたようなので、もう不要かな?　発言フィルタの位置をfixedにする機能だけ残したものにした。madpeople-fix-message-filter.user.js

関連

• 人狼用の他のGreasemonkeyスクリプト
  • Greasemonkeyで人狼BBSの発言数カウント他
  • 人狼審問 発言ポップアップ Greasemonkeyスクリプト

λ. 4日で学ぶモデル検査: 4日目

「プログラムのテスト」について。プログラム中にタイプミスをするよりは、プログラムのモデルを作る際にミスを犯す可能性の方がよほど多そうに思える。プログラムのテストを行うには、ソースコードからモデルを作成する部分をある程度自動化する必要があるように思う。

「自動販売機」については、面倒くさかったというのが最大の印象。仕様からきちんとしたモデルを作り検証するのはやっぱり大変。

……というわけで読了。いい本だった。続きの本が読みたいな。

λ. 『武装解除—紛争屋が見た世界』 伊勢崎 賢治

を読んだ。 感想は後で書きたい。

関連

• 伊勢崎賢治氏インタビュー

λ. 「トランプの和と積のパズル」と様相論理

どう書く？.org に「トランプの和と積のパズル」という問題があった。

プログラムを書いて答えを求めることは難しくないのだけど、この手の問題を見るたびに様相論理で一般的に扱えないのかなと思ってしまう。 思っただけでちゃんと考えたことがなかったので、少し考えてみようと思う。

知識論理

こういうのを扱う様相論理として知識論理(Epistemic logic)がある。 知識論理は様相論理の一種で、□φを「φであることを知っている」と解釈する。 そして、知識論理の □ は様相論理でいうところの S5 様相になっていることが仮定される。これはつまり、以下の形の論理式が成り立つということである(ただし、◇φ := ¬□¬φ)。

K(φ,ψ) := □(φ→ψ) → □φ → □ψ

φ→ψ であることを知っていて、更に φ であることを知っているなら、ψ であることも知っている。

T(φ) := □φ → φ

φであることを知っているのなら、φである。

5(φ) := ◇φ → □◇φ

「φでないことを知らない」のなら、そのことを知っている。

さらに、ここから以下のようなことも言える。

D(φ) := □φ→◇φ

φであることを知っているなら、φでないことは知らない。

B(φ) := φ→□◇φ

φならば、「φでないことを知らない」ということを知っている。

4(φ) := □φ→□□φ

φであることを知っているなら、そのことを知っている。

背景知識

Num := {1..13} として、原子論理式の集合 { N({m,n}), S(m+n), P(m×n) | m,n∈Num } が与えられているとする。それぞれの意図している意味は次の通りである。

N({m,n})

二枚のカードの数字がm,nである。

S(n)

二枚のカードの数字の和がnである。

P(n)

二枚のカードの数字の積がnである。

以下のような論理式の集合Φが成り立つことを仮定する。

• ∨{ N({m,n}) | m,n∈Num }
• { N({m,n})→¬N({m',n'}) | m,m',n,n'∈Num, {m,n}≠{m',n'} }
• { N({m,n}) → S(m+n) | m,n∈Num }
• { N({m,n}) → P(m×n) | m,n∈Num }
• { S(n)→¬S(m) | m,n∈Num, m≠n }
• { P(n)→¬P(m) | m,n∈Num, m≠n }

問題の記述

これでようやく問題が記述できる。

ここでは複数の人が登場するので「φであることをXさんが知っている」ということを [X]φ で表す(各 [X] はそれぞれS5様相だとする)。 そうすると、Xさんが数字を分かることは α(X) := ∨{ [X]N({m,n}) | m,n∈Num } で表すことが出来る。

• Aさんは積を知っているので ∨{ [A]P(m×n) | m,n∈Num }
• 同様に、Bさんは和を知っているので ∨{ [B]S(m+n) | m,n∈Num }
• Aさんは(この情報だけでは)数字が分からないので ¬α(A)
• Bさんも(この情報だけでは)数字が分からないので ¬α(B)
• BさんはAさんが「分かりません」というのは分かっていたので [B]¬α(A)

これを聞いたあとのAさんが知っているということは、元のAさんが知っているということとは別なので、[A1] という様相で扱うことにする。

• Aさんが元々知っていた事はすべて知っているので、[A]φ → [A1]φ
• 今聞いた情報を知っているので [A1](¬α(B) ∧ [B]¬α(A))
• それを聞いて答えがわかっているので α(A1)

同様に、これを聞いたあとのBさんが知っているということを [B1] という様相で扱うことにする。

• Bさんが元々知っていた事はすべて知っているので [B]φ → [B1]φ
• 「Aさんに話した内容をAさんが知っている」ことを知っているので、[B1][A1](¬α(B) ∧ [B]¬α(A))
• 今聞いた情報を知っているので [B1]α(A1)
• それを聞いて答えがわかっているので α(B1)

どうやって解くか

こうやって論理式で記述できたら、後は定理証明器やモデル検査で答えが求まらないものだろうか。 それはまた今度考える。

λ. 任天堂、複製したDSソフトを起動する「マジコン」販売業者を提訴

特許・著作権・商標の侵害とかではなく、不正競争防止法でのアクセスコントロールの迂回装置にあたるかが争点なのね。ちょっと意外な感じが……

λ. 『整理HACKS!—1分でスッキリする整理のコツと習慣 』 小山 龍介

読了。 この手のHACKS本にはあまり興味を持っていなかったが、いくつかは参考になりそうなものがあったので読んで良かった。

04 ドキュメントスキャナーでデジタルデータに変換する

前々から欲しかったのだけど、ScanSnap買おうと思った。

06 SugarSyncで「どこでもオフィス」を実現する

SugarSyncは知らなかった。Dropboxに似ているけど、主な違いは任意のフォルダを同期できることと、iPhoneアプリが既にあること。結構いいかも。無料版が2GBだけど、上の紹介リンクからアカウントを作ると+500MBボーナス。

WebインターフェースはDropboxの方が全体的に使いやすいと思った。ダウンロードするときにファイル名の非ASCII文字が化けたりもするし。

iPhoneアプリは使いやすい。 ただ、音楽の再生機能があるからだと思うが、起動時にiPodで再生中の音楽を停めてしまうのは、ちょっと困り者だと思うけど。

30 IMEバーは上端中央に置く

「おお、これはいい」と思ったんだけど、Chromeのウィンドウを最大化すると、ちょうどタブと重なってしまう。

40 RSSリーダーで情報収集を仕組み化する

紹介されていた、Google Reader と動機できるiPhone用のRSSリーダーのFeedsを購入した。 同種のものには、Bylineというのもあるらしいが、どっちがよいのだろう。

52 通販を活用して生活をシンプルにする

文房具等の通販をしているぽちっとアスクルは知らなかった。 今度使ってみよう。

73 マインドマップを使って情報のネットワークをつくる

そういえば、「マインドマネージャ」は勝間本でも紹介されてたな。

85 個人のオリジナル名刺をつくる

名刺作成サービスのアイボスは今度使ってみようと思った。