Alloyで人生モデリング その1：時間を含まない関係

人生モデリングの目的は、時間概念の扱い方を練習することですが、まずは時間を含まない関係の定義をやってみます。ここで考える対象物は人（human）なので、関係とは親子、夫婦、兄弟などです。

僕はAlloy経験が浅いので、Alloyのコード（モデル記述）をどのように書くのがいいのかよく分かりません。とりあえず次の方針にします； x.foo のような書き方が「xのfoo」と読めるようにします（なるべく）。例えば、p.mother は「pの母」と読みます。母（生みの親）は一人だけど、子供は複数かも知れないから w.children、なーんて考えるのがめんどくさいので、いちいち複数形は使わずに w.child とします。

内容：

1. 人、男、女
2. 基本は親子と夫婦
3. 誰にでも母親はいるのか？
4. 近親結婚の禁止
5. 時間概念の欠如

人、男、女

人は男か女のどちらかであることを次のように定義します。

-- 人生
module human_life

-- 人
abstract sig person {}

-- 男
sig man extends person {}

-- 女
sig woman extends person {}

pred show {}

/* コマンド */
run show

これだけでも実行（解析）できて、Alloy処理系は、人が3人以下の場合の男女の組み合わせを列挙します。

基本は親子と夫婦

これから、姻戚も含めた家族・親族の関係を定義するのですが、なにを基本関係にすればいいでしょう？ -- 次の2つを基本とすることにします。

1. 親子関係 p.mother ：人pの母親の集合
2. 夫婦関係 m.wife ：男mの妻の集合

とりあえず、何の制約もかけずにmotherとwifeの宣言だけをしておきます。

-- 人生
module human_life

-- 人
abstract sig person {
 mother: woman
}

-- 男
sig man extends person {
 wife: woman
}

-- 女
sig woman extends person {}

pred show {}

/* コマンド */
run show

実行すると、次の例が見つかりました。

男一人、女二人の例ですが、かなりムチャクチャなことになっています。

1. 男の妻はお祖母ちゃんになっている。
2. お祖母ちゃんの母親は自分自身になっている。

近親結婚を禁止するのは（Alloyの記述として）けっこう面倒なので後回しにして、まず、自分が母親になるケースを禁止しましょう。

-- 人生
module human_life

-- 人
abstract sig person {
 mother: woman
}

-- 男
sig man extends person {
 wife: woman
}

-- 女
sig woman extends person {}

-- 母親は自分ではない
fact mother {
 no (mother & iden)
}

pred show {}

/* コマンド */
run show

こうすると、お互いに母親という循環的関係が出てきてしまいました。甘かった。では：

-- 人生
module human_life

-- 人
abstract sig person {
 mother: woman
}

-- 男
sig man extends person {
 wife: woman
}

-- 女
sig woman extends person {}

-- 母親は自分ではない
fact mother {
 no (^mother & iden)
}

pred show {}

/* コマンド */
run show

^mother は母子関係の推移的閉包なので、それが自分を含まないことから循環を禁止できます。

実行すると、… アレ？ personが空集合になってしまった。それ以外の例はなし。ウーム（次に続く）。

誰にでも母親はいるのか？

このモデルに出てきているmotherは、生物学的な生みの親です。どんな人にも一人だけ母親がいるはずです。しかし、Alloyモデリングではこの仮定ではうまくいきません。

もし、誰にでも一人だけ母親がいるとすれば、ある人から「母親→母親→母親→ …」とたどっていくと、無限の系列ができます。しかも、この系列は循環しません。無限の女性がいないと、無限に長い母系列は作れません。Alloyのモデルインスタンスは有限なので、これが満たされることはありません。

しかたないので、母親がいないケースも認めます。実際には母親がいるのですが、ある範囲の集合には入っていないと考えましょう。そうすると、mother: lone woman と宣言を直すことになります。ついでに、すべての男に妻がいるわけでもないので、wife: lone woman にしておきます。

-- 人生
module human_life

-- 人
abstract sig person {
 mother: lone woman
}

-- 男
sig man extends person {
 wife: lone woman
}

-- 女
sig woman extends person {}

-- 母親は自分ではない
fact mother {
 no (^mother & iden)
}

pred show {}

/* コマンド */
run show

おっ、典型的な3人家族（夫婦と娘一人）が生成されましたよ。

でも、近親結婚や一妻多夫の例は出てきてしまいます。一妻多夫の禁止は簡単で、夫の集合husbandをwifeの逆として定義し、husbandの多重度も高々1（lone）にします。

-- 人生
module human_life

-- 人
abstract sig person {
 mother: lone woman
}

-- 男
sig man extends person {
 wife: lone woman
}

-- 女
sig woman extends person {
 private husband: lone man
}

-- 母親は自分ではない
fact mother {
 no (^mother & iden)
}

-- 一夫一婦
fact married_couple {
 husband = ~wife
}

pred show {}

/* コマンド */
run show

husbandにprivateを付けているのは、単に視覚化したときの絵が煩雑にならないようにです。

近親結婚の禁止

どこまでを近親とするかが問題ですが、あまり深く考えずに次のようにします。

1. 男は、自分の母、祖母などは妻にできない。
2. 男は、自分の姉妹は妻にできない。

これだと叔母さんや従姉妹との結婚は許されますが、あまり細かいことは言わない方向で。

まず、母、祖母などは、motherの推移的閉包に入るので、母系の祖先は ^mother と書けます。

男女の別やどっちが年長かなどは無視して「兄弟である」は次のように定義できます。（自分自身も兄弟のなかに含まれます。）

• p.sibling = p.mother.~mother

q in p.~mother は p in q.mother なので、~mother を child と定義しておくほうがわかりやすいでしょう。すると：

• p.sibling = p.mother.child

日本語で言えば：

• 人pの兄弟（の集合）とは、人pの母の子供（の集合）

以上のことから、次の制約で近親結婚を禁止できます。

1. m.wife と m.^mother に共通部分があってはならない。
2. m.wife と m.sibling に共通部分があってはならない。

まとめると以下のようになります。

-- 人生
module human_life

-- 人
abstract sig person {
 mother: lone woman,
 private sibling: set person
}

-- 男
sig man extends person {
 wife: lone woman
}

-- 女
sig woman extends person {
 private husband: lone man,
 private child: set person
}

-- 母親は自分ではない
fact mother {
 no (^mother & iden)
}

-- 一夫一婦
fact married_couple {
 husband = ~wife
}

-- 子供と兄弟の定義
fact child_sibling {
 {
  child = ~mother

  sibling = mother.child
 }
}

-- 近親結婚の禁止
fact forbit_intermarriage {
 no (wife & ^mother)
 no (wife & sibling)
}


pred show {}

/* コマンド */
run show

これで、現実に近い関係が定義できました。Alloyアナライザーは、3人までの人（空集合の0人もある）の集まりを次々に生成します。夫婦だったり、子・親・祖母だったり、赤の他人だったり、色々なパターンがありますが、変な例はなくなります。

ですが、run {#person =5} for 5 とかすると、ちょっとアヤシイ事例も出来てます。次は、男が姪を妻にしている例です。これは、姪や従姉妹との結婚を禁止してないので、しょうがないですね。

時間概念の欠如

以上に定義したモデルでは、母はいても父（母の夫）がいないケースがあります。父母が離婚したのかもしれません。それならば、過去に母の夫だった人を探せば父が見つかるかもしれません。また、父がいるとしても、再婚の結果の（血の繋がりはない）父かも知れません。これも過去がないと調べようがありません。

人間のあいだの関係は、時間とともに変化するし、「母のかつての夫」とか「未来の妻」とか時間を含む概念もあります。そこで、次は時間を扱ってみたいと思います。