bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

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

さて、スタート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は、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。