Alloyで書こう：私は彼？

Alloyでパズル(1)、(3) に解説を加筆した流れで。
ふだん言葉にしていない部分もしっかり書こうという話。
仕事を海外発注する場合に限らず、言ってない・書いてないところにバグは潜むもの。
さすがにパズルではなさすぎるので、Alloyでパズルシリーズとは別とした。

問題

Alloy本 A.3.1 驚くような三段論法 より

Doris Day の歌に、次のような節がある。
　　“Everybody loves my baby
　　 but my baby don’t love nobody but me."
　　みんな私の彼が好き
　　でも彼は私以外好きじゃない。
David Gries が指摘したところによると、論理的に厳密な立場からすれば、これは「私は私の彼だ」を含意しているそうだ。
(中略) Doris Day が言いたかったであろう形に記述し直し、今度はアサーションが反例を持つことを示せ。

書いてみる

例1

できる限り勝手な解釈を入れずに、そのまま書くとこうなるだろう。

sig Person {loves: set Person} { MyBaby in loves }
one sig Me in Person {}
one sig MyBaby in Person {} { no loves & Person-Me }

run {}
check { Me = MyBaby }

確かに言葉通りなら、彼は（彼が好き かつ 私以外好きじゃない）ので「私＝彼」でないと成り立たない。

例2

常識的に考えると「言いたかったであろう形」はこんな感じか。

sig Person {loves: set Person-this}     // 自己愛について話してない
one sig Me,MyBaby extends Person {}     // 私と彼は別人

pred everybodyLovesMyBaby {             // (彼以外の)みんなは彼が好き
    (Person-MyBaby) in loves.MyBaby
}
run everybodyLovesMyBaby

pred myBabyLovesNobodyButMe {
    MyBaby.loves = Me                   // 彼は私だけが好き
}
run {
    everybodyLovesMyBaby && myBabyLovesNobodyButMe
} for 5

例3

しばらくして思った。
いや違う、そんなにくどい解釈が言いたかったことじゃない。
こうか。

let everybody = Girl            // "everybody" means "every girls"
sig Girl {loves: set Boy}       // loves: lone Boy の方が気持ちに合っているかも
sig Boy {loves: set Girl}
one sig Me in Girl {}
one sig MyBaby in Boy {}

fact {
    everybody in loves.MyBaby   // Everybody loves my baby
    MyBaby.loves = Me           // my baby don’t love nobody but me (He loves only me)
}

run {} for 4 but exactly 4 Girl
check { Me = MyBaby }

BoyとGirlという概念が現れた（今の時代なら同性愛も念頭におくかもしれないが..）

例4

ちなみにあえて空気を読まずに「私以外好きじゃない」に戻すと

let everybody = Girl            // "everybody" means "every girls"
sig Girl {loves: set Boy}       // loves: lone Boy の方が気持ちに合っているかも
sig Boy {loves: set Girl}
one sig Me in Girl {}
one sig MyBaby in Boy {}

fact {
    everybody in loves.MyBaby   // Everybody loves my baby
    no MyBaby.loves & (Girl-Me)　// my baby don’t love nobody but me
}

run {} for 4 but exactly 4 Girl
check { Me = MyBaby }

私も好かれてなかったという身もふたもない解釈が出る（私が好きとは言ってない）。

なお、例1以外では check は「左辺と右辺は＝になりえないって定義してるよね」と警告される。

== is redundant, because the left and right expressions are
always disjoint.
Left type = {this/Me}
Right type = {this/MyBaby}

まとめ

言葉にされていない部分を仕様化・実装すると、例え意図をくみ取ろうとしてもこれだけ解釈が揺れる。
だから人に何かを頼むときは、できる限り正確で曖昧さのない仕様を書こう。
たぶんそれは、日本語や英語だけでは難しい。

参考

• Daniel Jackson：抽象によるソフトウェア設計 ―Alloyではじめる形式手法