抽象によるソフトウェア設計 付録A 練習問題 その14

付録A 練習問題続きます。A.3 の古典的パズルに入ります。

  • A.3.1 驚くような三段論法
    • まず歌詞の通りにモデル化してみる
sig Person { like: set Person }

pred doris_day (i, he: Person) {
    // みんな彼(he)が好き
    all p: Person | he in p.like
    // 彼(he)はわたし(i)のことだけが好き
    he.like = i
  }

assert DavidGriesInsight {
  all i, he: Person |
    doris_day [i, he] => i = he
  }
check DavidGriesInsight
    • 述語を本来の意図になるように変更してみる。要は「みんな」に「彼」が含まれてるのが問題だったので除く
pred doris_day_really_want_to_say (i, he: Person) {
  // みんな(彼を除いて)彼が好き
  all p: Person | he == p or he in p.like
  // 彼はわたしのことだけが好き
  he.like = i
  }
assert AssertForNewPred {
  all i, he: Person |
    doris_day_really_want_to_say [i, he] => i = he
  }
check AssertForNewPred
  • A.3.2 天井と床 
sig Flat {}
sig Person { ceiling: lone Flat, floor: lone Flat }

pred OneMansCeilingIsAnotherMansFloor {
  all disj p1, p2: Person | one f: Flat |
    f in p1.ceiling => f in p2.floor
  }

pred OneMansFloorIsAnotherMansCeiling {
  all disj p1, p2: Person | one f: Flat |
    f in p1.floor => f in p2.ceiling
  }

assert AImplyB {
  OneMansCeilingIsAnotherMansFloor =>
    OneMansFloorIsAnotherMansCeiling
  }
check AImplyB
    • これは反例を持つ。それを防ぐには「すべての者は天井と床をもつ」という制約があればよさそう。しかしこれを実現するには無限に続く階層か(alloy では検査できない)、循環した構造が必要になるので本来の歌詞の意図とは外れる
sig Person { ceiling: one Flat, floor: one Flat } // lone を one に変更
  • A.3.3 床屋のパラドックス
    • 有名な「ある村の床屋は自分で髭を剃らないもの全員の髭を剃る」という矛盾する命題
    • (a) はサンプルに run を追加して動かすだけ
    • (b) モデルに女性(髭を剃る必要がない)を導入して矛盾を解消してみる 
abstract sig Person {
  shaves: set Man
  }
sig Man extends Person {}
sig Woman extends Person {}
one sig Barber in Person {}
fact {
  Barber.shaves = {m: Man | m not in m.shaves }
  }
run {}
    • (c) 床屋が存在しないことを許容することで矛盾を解消する方法。シグネチャではなく述語の中で床屋を定義する
sig Man { shaves: set Man }

pred shaving {
  lone barber: Man |
    barber.shaves = {m: Man | m not in m.shaves }
  }
run shaving
    • (d) 床屋が複数存在することで矛盾を解消する方法。Barber のシグネチャの one を取るだけでいい
sig Man { shaves: set Man }
sig Barber extends Man {}
fact {
  #Barber > 1
  Barber.shaves = { m: Man | m not in m.shaves }
  }
run {}
    • ただしこれは床屋全員の髭をそる相手をあわせて考えた時に満たしているだけで、個々の床屋に注目すると最初の命題は満たされていない