はてな使ったら負けだと思っている このページをアンテナに追加 RSSフィード Twitter

2012/03/20(火)

さらに引っ越しました

はてなブログもなんかあんまり機能が好き勝手作れない感じだったので、自前でHaskell+Yesod製ブログエンジン書いてそっちに引っ越しました。

こちら: これは圏です

裏側の説明など詳細記事は「初めてのブログ」を参照してください。

現時点では、

などの特色があります。特に、

  • 記事のタグ付け
  • 貼った脚注がちゃんと表示される機能

この二つは、ローンチ時のはてなブログにはなかった素敵機能です!やりましたね!

そんな感じで。ではでは。

2012/01/09(月)

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

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

これがそこです:これは圏です(はてな使ったら負けだとおもっていた)

さようならさようならー

2011/09/22(木)

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

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

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

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

補足

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


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

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

2011/08/30(火)

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:ちょっと何云ってるのかわからない感ある

2011/08/29(月)

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

f:id:mr_konn:20110829210749p:image

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

f:id:mr_konn:20110829221207p:image

図を見てみると、確かに性別が女性のときだけ「はい」、男性は「いいえ」と答えるようになっていますね。よかった!

では、どんな質問なのか?「評価」関係を基に見てみると……

性別服装質問の値答え

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

舞台裏

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

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

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

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

抽象によるソフトウェア設計−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:実際に男の娘が手に入るかは保証しませんが!