シグネチャのフィールドにある関係の多重度

さて、スタートAlloy中、頂いたテクニカルな質問のうち1つに、当日うまく答えられませんでした（すいません… orz）。

ちゃんと考え直したので(^^; ここに書いておきます。（thx to @masahiro_sakaiさん）

以下のようなシグネチャ宣言があったとする。

sig A {
  r: B one -> one C
}

ここで、Bのスコープを1にすると、任意の a: A から得られる a.r が全部同じになってしまう。
たとえば、以下のようなコマンドで反例が出ない。

check {
  all disj a1, a2: A | a1.r = a2.r
} for 3 but 1 B

たとえば a1.r は空で、a2.r は空でないような可能性があるように思うが、なぜないのか？

まず、シグネチャのフィールドにある関係は、次のように解釈されます。（Alloy本 p.261）

…したがって、例えば
sig S {f: e}
という宣言によって導入される制約は、（fを通常の変数とした場合の）fが式eの部分集合であるという制約ではなく、以下のような制約になる。
all this: S | this.f in e

よって、先ほどのシグネチャA内のフィールドrの宣言は、

all a: A | a.r in B one -> one C

という制約だと解釈されます。（thisはaに置き換えました）

更に、関係の中の多重度についてですが、（Alloy本 p. 76）

多重度は単なる省略記法であり、標準的な制約に置き換えることができる。以下の多重度制約は、
r: A m -> n B
以下のように書き換えることができる。
all a: A | n a.r
all b: B | m r.b

とあります。コロンは in と読み替えても意味的には同じです。

ということで、先ほどの制約式を、更に展開すると

all a: A | all b: B | one b.(a.r)
all a: A | all c: C | one (a.r).c

となります。

なので、Bのスコープが1だと、B、C ともに空で a.r が常に空になるか、B、C ともにサイズ1で、aによらず a.r が存在して一意に定まるか、いずれかになります。

bonotakeの日記