試しに日記を書く

取り敢えず一日坊主を回避すべく日記を書こうと思う。

思うんだけど書く内容がない。なにせ、

11：30 ごろ

起床

12：00 ごろ

多分御飯を食べおわる

12：00〜13：20

ベッドに籠って寝るかと思いきやひたすら Toobz に打ち興じている内に時間が過ぎる

13：20ごろ

このままではいけない、読書会のレジュメを書くんだと思い立つ。

13：20〜13：50

移動

13：50〜14：19

ハニーラテ&ミルフィーユと格闘。最近ミルフィーユばかり食べているので、次来たときはミルクレープにするぞと糖分を省みない決断をする。

14：20〜17：00

読書会レジュメ執筆。

17：00

隣に座った高校生カップルがチラチラこちらを見、時折クスクス失笑しているのを物ともせず、実際かなり気にしつつも執筆してきたがそろそろ席を離れたい、しかしこのまま席を離れたら負けな気がする……と思っていたらカップルが席を立ち、やがて愛機 MacBook の充電も切れかかってきたのでこれ幸いと席を立つ。

17：00〜17：10

電源を求めて最寄りの図書館に赴くが、17:20 閉館と知りすごすごと引き返す。その途中で円城塔の新刊が amazon で予約出来ることを知り予約。iPhone ばんざい。

17：10〜17：20

電源を求めて更にショッピング・モール内をうろつく。ドーナツ店とチキン屋に電源が無いことは知っている。喫茶店内を伺うがよく見えない。店員が寄って来そうだったので慌てて入口を離れるが、外から店内を伺ったりちょっとした不審人物である。近くの出入口から出ようとしたが最初と違う扉から出て仕舞ったみたいでどこだかわからない。外でヤンキーが吠えている。こわい。店内に取って返す。出口が見付からない。とても惨めな気持になる。死にたい。産まれこないほうがよかった。せめてもと思って先程かってに玉砕した喫茶店に戻る。店員さんに「電源タップ使用出来る席はありますでしょうか……？」。少々お待ちください、と店員さんが奥へと消える。しばらくして戻ってきて「ないみたいです」そうですか。僕は恰度目の前にある電源コンセントを眺め駅へと帰る決意をしたのだった。

17：20〜17：45

帰途に就く。

17：45〜18：50

鍋の準備をする母上を尻目に Scala の勉強をそれとなくしながらビン=ラディン暗殺のドキュメンタリーを観る。面白い。虐殺器官読み返したいなあ。TV『特殊部隊は射殺するかしないかの判断を一瞬で行うよう訓練されています……』母「あんたも訓練してもらったら」なんと答えたかは忘れたが読み返したいので貸した虐殺器官を早く読めとは云った筈である。ビン=ラディンひとりの暗殺がこれだけ英雄視されているのだから、チャップリンの「数が殺人を正当化する」仮説は否定されたな、などと考える。父上が帰宅。

18：50〜19：20

鍋を食べる。豚と水餃子。とまとポン酢。タラコ。うまい。ニュースで報じられていた内閣支持率が見事に線型に減少していて関心する。

19：20〜20：00

Scala の勉強をする。疲れたので一旦休み宣言をする。風呂に入って原稿をやると云う

20：00〜現在

大方の予想通り特に風呂に入りもせずずっとついったーに現を抜かす。はてなブログ書くかと思い立つ。今書いてる。

これが今日やったことの全てだ。驚くほどに何もない……と書こうと思ったが一々書いていたらやたら長くなってしまってちょっと盛り沢山の一日を送っているように見える。しかしよくよくみると大抵が自我の範囲内で完結していることに気付く。とくにこれといって特筆すべき、ドラマチックな事件などはない。

ちなみにこのタイムテーブルは Twitter のログを見ながら書いた。特に変わったことをしなかったので記録から簡単に復元出来た。それが良いことなのか悪いことなのかはわからない。どの時間帯に飯を喰ったのかだけ、若干迷った。ちょっと詳細すぎて住処が簡単に割れてしまいそうな気がしたので、もうこんな詳細には書かないほうがよいかもしれない。

やってみて、Twitter のお陰でだいぶ簡単に日記が書けそうなことがわかった。とすると案外今後も簡単に続けていけるかもしれないが、しかし、それなら Twitter の方をお読み下さいで済むのではないか、と云う疑念も拭い切れない。「うんこうんこー」とか「ちんこちんこー」とかそういう雑音が省かれている分こうしてまとめてみるのは意義があることなのかもしれないが、そうした言葉を今ここに書いてしまったし最早無意味かもしれない。専門家の意見を待ちたいところだ。

念のため、今日のこれからの予定を下に書く。

1. 風呂に入る
2. 歯をみがく
3. 原稿を書く
4. といれにゆく
5. 明日の準備をする
6. 寝る

本当にこの通りに進むかどうかは知らない。多分大方の予想通り進まない。いや、こんな簡単な予定表一つ守れないでどうするのだと云う指摘もあろうが、そんなことは知らない。知らないといったら知らない。

はてなブログはじめました

なんか知らない内にはてなブログが一般公開になったのでこれから暫くこっちを使ってみようと思います。
まあいつのまにかとってあった http://www.konn-san.com/ のほうでブログを建てようかなあ、と云う説もあったのだけど暫くこっち、と云うことで。Haskell 関連の話題も、Haskell グループの方で書いてたけどこっちにしようかなぁ、わからない。
Haskell 系の話題だけ konn-san.com と云う可能性もありうる。あ、konn-san.com はかなり未完成なので見にいかないほうがいいです。

で、なんだっけ。
そう、はてなブログをはじめましたって云う話でした。見りゃわかるよ。どうぞ御贔屓に。ひょっとしたら日記めいたものを付け初めるかもしれないけどまあ、Twitter をやっているのでそっちに時間を取られてここに書くことはない気もする。だいいち日記に書くほどのことがあるのかと問われてだいぶ怪しい。

そうだ、そういえば新年でしたね。新年なので新年の抱負でも。

数学を頑張って（頑張るってなんだ）、人間として生きて、ちょっと創作に力を入れてみる。

こんな感じですかね。なんか周囲の人間が文化的な活動を送っているのに比して自分はひがな一日寝てるか、ひがな一日寝てるか、ひがな一日寝てるかなので、これは大変よろしくない。なにがよろしくないといって寝るいがいに能もないので、もし罷り間違って恋人のようなものが出来たときに、さてデートどこにいこうか、しかして文化的な場所をしらない、よし昼寝だ、と云う体たらくで一日と待たずに破局離縁よ！と云うことになり兼ねない。そこ、恋人が出来よう確率など殆んどゼロだとかそう云うことを云わない。

まあだもんで、日記に書くために文化的な生活を送ろうと思う。書くかわからないけど。

と云うひどく結論めいたものが出て終わると思ったらそうは問屋が卸さない。商売上がったりです*1。

まず日記を書くとして問題になりそうなことを論うてみたい。

だいいちに*2、何を書くのか？今のところ家で寝ているか大学にいるかラウンジで駄弁っているか飯喰ってるか家で寝ているかごく稀に大学の勉強をしているかくらいしか行動パターンがない。それを一々書いても大して面白みもなかろうし、それくらいなら何もこんなところに書かずとも Twitter に垂れ流せばよいだけのはなしだ。

だいにに、どこまで書くのか？よしんば何か楽しいことがあった、悲しいことがあった、嬉しいことがあった、恥ずかしいことがあった、ねこなことがあった、あんなこといいな、できたらいいな、そんなことがあっても、どこま書くべきなのかと云うのは一般に自明でないだろう。どこまで名前を出すべきか？常識に照らして実名はよくない。では頭文字ならよいのか？それでもわかるひとにはわかるし、イニシアルトークと云うのは部外者からしてみたら面白くとも何ともないものだ。まあ、周囲の人間をつぶさに観察して考えるに、こいつらの奇行と云うものは中々に面白くキチガイじみていて中々お目に掛かれるものではないと思うが、それにしたって不特定多数にとって縁もゆかりもない人間の奇行を書いて万人を楽しませることが出来るかと問われてその自信はない。もっとも楽しませる目的で日記を書くというのも妙な話ではある。また、プライヴァシーだかプライマリーだかに照らして考えても、イニシアルだけ出しても十分に情報漏洩であり、彼/彼女がそうした記述を好むかどうかと云うのは非常にデッリケートな問題だ。そんなところに促音は入らない。

だいさんに……と色々列挙することも出来るがこのあたりにしておこう。何故ならもう飽きてきたし、お風呂に入りたい。

はてなブログに引っ越します

なんか知らん内にはてなブログがローンチされていたので、しばらくはてなブログに引っ越すことにします。本当はなんか http://www.konn-san.com/ にブログでも建てようかなと思っていたのだけど。

これがそこです：これは圏です（はてな使ったら負けだとおもっていた）

さようならさようならー

社内セミナーで Alloy Analyzer について発表してきました

PFI の社内セミナーで Alloy Analyzer について発表してきました。

Alloy Analyzer のこと

View more presentations from Hiromi Ishii

なんか ust でストリーミング放送された上、録画・保存されてしまっているらしいので、観てやろうという酔狂な方は下からご覧になったらいいんじゃないでしょうか。

なんだか台本とか特に考えずに書いたので、早口かつしどろもどろと云うか何か何云ってるのか良くわからない感じになっちゃってますね……反省。

補足

日本語をソースで使うには、4.2RC を使う必要があります。

さて。訳者の一人でいらっしゃる id:bonotake さんやさかいさんから幾つか補足がありましたので紹介します。

• 発表では「有界モデル検査器」と紹介しましたが、公式には「有界モデル発見器」と呼ぶそうです。
• 発表では assert を「不変条件」と表現していましたが、より広い概念なので「表明」とか「アサーション」と表現する方が適当でした。
• 矛盾したファクトを判別する方法がありました。
  • MiniSAT が使える環境では、MiniSat with Unsat Core を SAT Solver に指定すると、矛盾する箇所をハイライト出来ます
  • Options Menu の Unsat Core Minimization Strategy で矛盾箇所の粒度/速度を指定出来ます

Alloy でクリプキ可能世界意味論！

Alloy でクリプキの可能世界意味論をエンコードしてみた記録。
論理学をきちんと勉強した訳じゃないので、もし誤りがあったら是非教えてください。

可能世界意味論と云うのは、偉大な論理学者ソール・クリプキが、なんと高校生の頃に思い付いた様相論理の意味論です。
様相論理って云うのは、通常の命題論理に、「□P (必然的に P)」とか「◇P (Pであることが可能)」と云う二つの記号を付け加えて出来る論理体系です。要は可能性を扱う論理学ですね！

ひとくちに様相論理と云っても色々種類があるそうで、「必然的にP なんだったらどう考えてもPだろうよ」「必然的にPであるためにはまずPが可能じゃないといけないんじゃね？」「必然から可能が必然だよな*1！」とかみんな色々な法則を提唱してるんだとか。みんながみんなオレオレ様相論理を作るので、それぞれが一体どういう関係にあるのか？とか、本当にそれで大丈夫なの？とか、混沌とした状態ですね。

そこに光明を齎したのが若き日のクリプキで、「可能世界同士の二項関係を考えればいいよな！」と云う一言で各体系の関係を綺麗に纏め上げてしまったのだそうです。すごい！

それがクリプキの可能世界意味論。平たく説明すると、

1. 沢山の「可能な世界」の集合とその間の"到達"可能性を考える。
2. ある世界 w で「P が必然的」であるとは、w から到達可能な全ての世界で P が成立すること
3. 同様に「Pが可能」であるとは、w から到達可能な世界のうち少なくとも一つで P が成立すること

と云う考え方に基いています。到達可能性は世界同士の二項関係で、色々と提唱されてきた様相論理の公理は、二項関係が満たす性質と一対一に対応するよ、と云うのがクリプキの発見でした(ですよね？)。

例えば、反射律(a R a)と「必然的にPならP」と云う命題、推移律(a R b, b R c ⇒ a R c)「必然的にPなら必然的に『必然的にP』」と云う命題がそれぞれ対応していたりします。

と云う訳で、それを Alloy で書き下してみたのが以下のソースです。

module possibleworld

sig World {}
sig Atom {}
enum TruthValue { True, False }

sig KripkeFrame {
  worlds : some World,
  accessible: World -> World
}

abstract sig Formula {}

sig Atm extends Formula { atom : one Atom }
sig Neg extends Formula { var: one Formula }
sig Imp extends Formula { left, right: one Formula }
sig Nec extends Formula { var : one Formula }
sig Pos extends Formula { var : one Formula }

fact NoRecursiveFormula {
  no iden & ^(Neg <: var + Nec <: var + Pos <: var + left + right)
}

sig Model {
  frame : one KripkeFrame,
  valuation: World -> Atom -> one TruthValue,
  eval : World -> Formula -> one TruthValue
} {
  (valuation.univ).univ in frame.worlds
  (eval.univ).univ  in frame.worlds
  
  all w : frame.worlds {
    all exp : Atm |
      eval[w, exp] = valuation [w, exp.atom]
    all exp : Neg |
      eval[w, exp] = True <=> eval [w, exp.var] = False
    all exp : Imp |
      eval[w, exp] = True <=>
        (eval [w, exp.left] = False or eval [w, exp.right] = True)
    all exp : Nec |
      eval [w, exp] = True <=>
        all w' : frame.accessible[w] | eval [w', exp.var] = True
    all exp : Pos |
      eval [w, exp] = True <=>
        some w' : frame.accessible[w] | eval [w', exp.var] = True
  }
}

pred valid(m : Model, A : Formula) {
  all w : m.frame.worlds | m.eval [w, A] = True
}

pred valid(f : KripkeFrame, A : Formula) {
  all m : Model | (m.frame in f) => valid [m, A]
}

one sig atmP, atmQ in Atom {}

one sig P in Atm {} { atom in atmP }
one sig Q in Atm {} { atom in atmQ }
one sig NecP in Nec {} { var in P }
one sig NecQ in Nec {} { var in Q }
one sig PosP in Pos {} { var in P }

one sig PimpQ in Imp {} { left in P and right in Q }
one sig NecPimpQ in Nec {} { var in PimpQ }
one sig NecPImpNecQ in Imp {} { left in NecP and right in NecQ }
one sig K in Imp {} { left in NecPimpQ and right in NecPImpNecQ}

one sig D in Imp {} { left in NecP and right in PosP }

one sig T in Imp {} {left in NecP and right in P}

one sig NecNecP in Nec {} { var in NecP }
one sig Four in Imp {} { left in NecP and right in NecNecP }

one sig NecPosP in Nec {} { var in PosP }
one sig B in Imp {} { left in P and right in NecPosP }
one sig Five in Imp {} { left in PosP and right in NecPosP }

fact {some Model}

-- K : □(P → Q) → (□P → □Q)
assert Kは常に成立 {
  all f : KripkeFrame | valid [f, K]
}
check Kは常に成立 for 5

-- D : □P → ◇P
assert Dとserialの同値性 {
  all f : KripkeFrame |
    (all w : f.worlds | some f.accessible [w]) <=> valid [f, D]
}
check Dとserialの同値性 for 5

-- T : □P → P
assert Tと反射律の同値性 {
  all f : KripkeFrame |
    iden in f.accessible <=> valid [f, T]
}
check Tと反射律の同値性 for 5

-- 4 : □P → □□P
assert Fourと推移律の同値性 {
  all f : KripkeFrame | let r = f.accessible | 
    r.r in r <=> valid [f, Four]
}
check Fourと推移律の同値性 for 5

-- B : P → □◇P
assert Bと対称律の同値性 {
  all f : KripkeFrame | let r = f.accessible | 
    ~r in r <=> valid [f, B]
}
check Bと対称律の同値性 for 5

-- 5 : ◇P → □◇P
assert Fiveとユークリッド律の同値性 {
  all f : KripkeFrame | let r = f.accessible |
    valid [f, Five] <=>
      all w, w', w'' : f.worlds |
      w -> w' + w -> w'' in r => w' -> w'' in r
}
check Fiveとユークリッド律の同値性 for 5

スコープを 5 までにしても、それぞれの assertion 反例は見付からないので、ちゃんと成立しているとみて良さそうですね！わいわい！

参考文献

可能世界意味論に関しては、この本の末尾の方をぱらぱら捲りながら書きました：

論理学をつくる

まだ読んでいる途中ですが、論理学の基礎から発展的な内容まで、1から丁寧に解説した self-contained な教科書です。語り口も軽妙で、読んでいると論理学って楽しいなあ、と云うのをしみじみと感じます。興味を持たれた方は是非。

*1:ちょっと何云ってるのかわからない感ある

Alloy で男の娘を見付けよう

問題

どこかの国の非実在学園での話と思ってちょーだい。

この学園には四種類の人間が通っているそうです。男の子、女の子、男の娘、男装の麗人だそうで。自由な校風なんですね。

自由なのは結構なんですが、時偶あるのが、かわいい女の子だ！と思ったら実は男の娘でしたと云う悲劇で、人によっては美味しいシチュエーションなんでしょうが、少なくともぼくは女の子のほうがいいです。野郎は野郎なので……。ただ、学ラン着てる女の子とか倒錯してていいかんじだなあ、と思うので、男装の麗人はうぇるかむですね！わいわい。

と云う訳で、何とかして性別を判定したいんですが、はて……。

ところで、いかに自由な校風と云えど、一つだけ校則があるそうです。曰く、「嘘吐きは須く嘘を吐き、正直者はみな真実のみを喋るべし」。この法則は受け答えだけでなく、日常の所作や言動にも適用されるそうで、従って男の子や女の子は常に真実を、男の娘や男装の麗人は常に嘘だけを喋ることになります。

これを使って何とかして女性だけを見付けられないでしょうか？あとしつこい男は嫌われるので、イエス・ノーで答えられる質問一つだけで見分けられると良いんだけど……と云うのが問題。

解説

この問題の原典は、『スマリヤンの決定不能の論理パズル―ゲーデルの定理と様相理論』の第五章で出て来る金星人と火星人のパズルです。原典では「金星人の女性は常に真実、男性は常に嘘を喋り、火星人はその逆」と云う設定です。そのまま使ってもよかったんですが、今っぽいサブカルネタを採り入れた方がウケるだろうと云う編集部のテコ入れによって男の娘パズルに姿を変えました。純粋に政治判断であって、ぼくが男の娘が好きってわけじゃないです。理解は出来ますが、やっぱりね……。寧ろ男装女子のほうが好きです！わいわい。

閑話休題。そのまま論理的に解いても良いのですが、今回はAlloy Analyzerを使います。

Alloy Analyzer と云うのは有界モデル検査器とよばれるものの一種で、仕様を記述するとそれを満たす有限モデルを列挙・可視化してくれるようなツールです。ソフトウェアの仕様や抽象化の漏れ・矛盾が無いかを確認するツールですね。

何やらようわかりませんが、こいつの裏では SAT ソルバが動いているので、リッチな SAT ソルバのフロントエンドと思っておけば間違いないです。

と云う訳で、早速 Alloy で記述してみたのが以下です*1。

module otokonoko
enum 男か女 {男, 女}
enum 真理値 {真, 偽}

sig 質問 {
  評価: 人間 -> one 真理値
}

abstract sig 人間 {
  性別: 男か女,
  服装: 男か女,
  回答: 質問 -> one 真理値
} {
  all q : 質問 |
    性別 = 服装 <=> 回答[q] = q.評価[this]
}

one sig 男の子 extends 人間 {} {
  性別 in 男 and 服装 in 男
}

one sig 男の娘 extends 人間 {} {
  性別 in 男 and 服装 in 女
}

one sig 女の子 extends 人間 {} {
  性別 in 女 and 服装 in 女
}

one sig 男装の麗人 extends 人間 {} {
  性別 in 女 and 服装 in 男
}

pred 女性発見器(何か: 質問) {
  all 誰か: 人間 | 誰か.性別 in 女 <=> 誰か.回答[何か] = 真
}

run 女性発見器

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

何だかごちゃごちゃして判りづらいですね。と云う訳で「質問」で射影して、要らないものを消してみます。

図を見てみると、確かに性別が女性のときだけ「はい」、男性は「いいえ」と答えるようになっていますね。よかった！
では、どんな質問なのか？「評価」関係を基に見てみると……

性別	服装	質問の値	答え
男	男	偽	偽
男	女	真	偽
女	男	偽	真
女	女	真	真

と云う関係にあるみたいです。よくよく見てみると、性別関係なく、服装が女性であるときだけ質問は真になっているので、求める質問は「あなたは女性の服を着てますか？」が答えと云うことになります。よかったね*3！

舞台裏

なんでこんなことを考えていたのかと云うと、社内発表で Alloy について喋ろうと思ってたんですが、Alloy のメインの用途と云っても過言ではない*4、論理パズルソルバとしての例が資料に欠けてることに気付いたわけなんですよ。

最初は有名な Kalotan パズルをやろうと思ったんですが、抽象化をどうしていいかわからずに「Kalotan パズルはAlloy に向いてない」などと安易に口走ったところ、bonotake さんの鉄槌を喰らってしまったので、これを参考にしつつ、何か知ってるパズルを解いてみようとしたのでした。

こういう、質問を探し出す"メタパズル"をどう解けばいいかなあ……と云うのを悩んでいると、ぼのたけさんから助言を頂いたので、それを参考にしつつ頑張ってみました。てへ ('-'*

この記事で Alloy に興味を持った方は、

抽象によるソフトウェア設計−Alloyではじめる形式手法−

を読むとAlloy の興味深く楽しい世界を知ることが出来るかと思います。僕もこれで勉強しています。
ウェブでも、id:m-hiyama さんや id:bonotake さん、さかいさんなどが Alloy の記事を書かれているので、参考にすると良いかと。

オマケ

ところで、世の中には「男の娘にしか興味ないんじゃい！」と云う末期の方々もいらっしゃると聞き及びましたので、その方々の為に「男の娘発見器」のソースも載せておきます。
さっきのの末尾にこれを追加して実行すれば、求めるものが手に入りますよ*5。

pred アッ男の娘だ(誰か: 人間) {
	誰か.性別 in 男 and 誰か.服装 in 女
}

pred 男の娘発見器(何か: 質問) {
	all 誰か: 人間 | アッ男の娘だ [誰か] <=> 誰か.回答[何か] = 真
}

run 男の娘発見器

これがどのような質問なのかは、自分でモデル生成して考えてみてください。
それでは、enjoy!

*1:日本語交ぜ書きをするには、最新の 4.2RC が必要です

*2:どうでもいいですが、『女性発見器』と云う言葉にモゾモゾしてしまった人、早く思春期を脱した方が良いですよ

*3:誰ですか、そんなん見ればわかるじゃんとか云ったのは？

*4:傍証：1 2 3 4 5

*5:実際に男の娘が手に入るかは保証しませんが！

生きてます