白と黒のとびら 第3章 復元 その3

ハマンの遺跡は第四十七古代ルル語に対応する遺跡だそうで

• 最後が〇●で終わる文字列をすべて文とみなす言語に対応
• 部屋は3部屋
• 入口と出口は別の部屋

そして遺跡の年代から

• 同じ部屋にある白と黒の扉の行き先が同じであることはない
• 同じ扉の行き先は一定

という制約がある。

ここから部屋の構造を推測するというので、このくらい簡単……と思いきや若干手間取りました。

module white_black/haman

sig 部屋 {
  白: one 部屋,
  黒: one 部屋
} {
  白 != 黒
}

one sig 入口 extends 部屋 {}
one sig 出口 extends 部屋 {}

pred ハマンの遺跡 {
  出口 = 入口.(^(白+黒)).白.黒
  no 出口 & 入口.(^(白+黒)).白
  no 出口 & 入口.(^(白+黒)).黒.黒
  no 出口 & 入口.白
  no 出口 & 入口.黒
}

run ハマンの遺跡 for exactly 3 部屋

出口に到達できる条件はいいとして、"*白黒" でない経路で出口に到達しない、という条件を 入口.(^(白+黒)).白 != 出口 と書いてしまったのですが、この書きかただと、行き先が出口のみになる場合のみ除外することになってしまいます。そうじゃなくて 入口.(^(白+黒)).白 で到達できる部屋の集合のなかに出口が含まれていない、というのが正しい条件なので no 出口 & ... という書きかたにしました。また ^rel は rel を 0回結合したものは含まれないので、入口.白 と 入口.黒 は個別に条件に追加しました。
あと、条件を良く読むと第四十七古代ルル語は「*〇●」で終わる文字列*全て*が文になるので、この遺跡も白、黒と辿ったら必ず出口に到達するはず……、なので出口に到達する条件は in ではなくて = で完全に一致するようにしました。

これで遺跡の構造は1つに決定できました。

とりあえず今日はここまで。本章では構造を推定する過程が物語で説明されているようなので明日はそれを粛々と読もうと思います。ちょっと先走りすぎたかな。