Alloyでパズル (14) 僕は僕のおじいちゃん

さてネタ切れというか、書いてまとめるのが間に合わなくなってきた。
今無料で受けられる N予備校 の「ものがたり創作」面白いです。
物語の構造を抽象モデル化して分析する話になっています。

今回は Alloy 本から、どう書くか以前に定義がどうあるべきかに悩まされた問題。
しかしそこを悩むときにこそ、「モデル発見器」とも称される Alloy の強みが発揮されると思っている。

問題

Alloy本 4.1 例題：自分が自身の祖父

『僕は僕のおじいちゃん』（“I’m My Own Grandpa”）という古いポピュラーソングがある。
一体どうやったらそんなことが起こるのか、Alloy を使って見ていくことにしよう。

リスト

『僕のおじいちゃん』とはどういう存在なのか、その定義が問題。

実親の実親が自分であることはあり得ない。
なので結婚とそれによって生まれる義理の親という関係を定義する必要があるが、誰との結婚が認められるかは国や時代によっても異なるだろう。
また、どこまでを義理の親と認めるかはおそらく法律的な話とは異なる。
結婚しないと子どもが生まれない訳ではないので、それを無視してもいけないだろう。

同性婚や重婚を認めた場合も、簡単な変更で試せるようにした。
「僕は僕のおじいちゃんではない」に対する反例を挙げさせる形とした。

// 僕は僕のおじいちゃん
// 義理の親の義理の父 までおじいちゃんと認定（親夫妻と配偶者の直親までを広義の親とした）
// 同性婚や重婚を許すと結果も増える
// 近親婚をどのくらい省くべきか不明だが、ありなら母と結婚するだけで成立する

abstract sig 人 {
    父: lone 男性,
    母: lone 女性,
    配偶者: lone 人,
    おじいちゃん: set 男性,
    おばあちゃん: set 女性
} {
    this not in this.祖先                   // パラドックス防止
    no 配偶者.祖先' & this.祖先'             // 近親婚防止１
//撤回    no 母.祖先' & 父.祖先'                   // 近親婚防止２
    おじいちゃん = this.親'.親' & 男性        // おじいちゃんとは
    おばあちゃん = this.親'.親' & 女性        // おばあちゃんとは
}
fact { 配偶者 = ~配偶者 }   // 双方向関係
sig 男性 extends 人 {} { no 配偶者 & 男性 }
sig 女性 extends 人 {} { no 配偶者 & 女性 }
one sig 僕 extends 男性 {}

let 親[p] = p.(父+母)
let 親'[p] = p.親 + p.親.配偶者 + p.配偶者.親   // Alloy本では親夫妻まで
let 祖先[p] = p.^(父+母)
let 祖先'[p] = p.*(父+母)   // p自身を含む

run { some 配偶者 } for 4
run { one おじいちゃん } for 5
check { no 僕 & 僕.おじいちゃん } for 4

Alloy本では兄妹婚や姉弟婚を禁止していないが、本リストでは「近親婚防止１」で省いている。

注）このリストはあくまで例であり、日本の法律や私の見解を示すものではありません

結果

提示される例を見て、不適切として除外すべきか判断するのにも苦労した。
「この例は子が生まれてから離婚して、元妻の母と再婚したと考えるべき？」など。

Alloy 本では２パターンだが、今回の定義では４パターンとなった。

1. 義理の父の義理の父
   

2. 義理の母の義理の父
   

3. 義理の父の義理の父
   

4. 義理の母の義理の父
   

追記

そういえば、「近親婚防止２」は「結婚しないと子どもが生まれない訳ではないので、それを無視してもいけない」に抵触している。
これを外すと図のような関係が出てくるが、倫理面はともかく現実にあり得るだろうからモデルから外すのは厳しすぎた。
（４人以内で母という関係が２つより多い run { #母>2 } for 4 で簡単に出てくる例）

「近親婚防止２」は撤回しよう。
あり得ない関係が出てくるようなら、それはまた別の修正ということで。
（近親婚防止と言いながら結婚に関係ない条件になっているのが、何かを物語っていた気も）

追記２

養子縁組によって生まれる親子関係を忘れていた。
これを考慮すると何か変わるか試してみるのもいいだろう。

参考

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