Alloy の３項関係における多重度指定について

Alloy についてまともに使えるようになろうと、最近ああだこうだやっている。
静的なモデリングについてはほぼ納得できた気がしているのだが、動的なモデリングについては、Timeイディオムあたりでどうも理解が追いつかずに止まってしまっていた。

なぜそこで止まるかと言えば、２項関係を扱う限りは多重度指定の意味が直感的に理解できるのだが、３項関係になると、指定した多重度の意味が一気に複雜なものになってしまうから、である。自分はそうだった。
ということで、３項関係において指定した多重度がどういう意味を持っているのか、を実際に検証してみたので結果を書いてみる。
なお、使用したバージョンは、Alloy Analyzer 4.2 である。

Alloy本での対応箇所

Alloy本（『抽象によるソフトウェア設計』）で、多重度指定に関する記述があるのは以下のあたり。
・p77 3.6.5 入れ子の多重度
・p262 B.7.4 Alloy言語リファレンス多重度

言語リファレンスの方が詳しいが、実例がないので少々理解しづらい。
３項以上の関係に関する記述としては、p263の「多重度キーワードは矢印式が入れ子になった場合でも使える」と書いてある箇所以降。これには後で触れる。

検証のやり方

・ A, B, C の３つのシグネチャを用意。
・３項関係、rel : A -> B -> C を宣言。
・ fact で rel についての多重度指定をさまざまなパターンで設定。
・各パターンについて性質を調査。

とした。
とりあえず今回は one だけで、キーワードの出現回数は１回の場合だけにした。

シグネチャの宣言まわり。
全てが1個以上ある条件にしたかったので some をつけてある。

some sig B {}
some sig C {}
some sig A {
rel : B -> C
}

対象のパターン。
one を置く位置で4パターン。カッコの付け方でそれぞれについて３パターン。計12パターン。

fact {
//rel in A one -> B -> C
//rel in A one -> (B -> C)
//rel in (A one -> B) -> C
//rel in A -> one B -> C
//rel in A -> one (B -> C)
//rel in (A -> one B) -> C
//rel in A -> B one -> C
//rel in A -> (B one -> C)
//rel in (A -> B) one -> C
//rel in A -> B -> one C
//rel in A -> (B -> one C)
//rel in (A -> B) -> one C
}

上記のパターンそれぞれについて、以下のような述語、アサーションで性質を確認した。
（util/ternary の関数を使用）

// rel に含まれない要素があるかどうか
pred existsAloneA {
some a : A | a not in dom[rel]
}
pred existsAloneB {
some b : B | b not in mid[rel]
}
pred existsAloneC {
some c : C | c not in ran[rel]
}
// A, B, C の全ての要素が rel に含まれているか
assert noExistsAlone {
not existsAloneA and not existsAloneB and not existsAloneC
}
// ある２項関係の全ての組が rel に含まれているか
assert allABInRel {
select12[rel] = A -> B
}
assert allACInRel {
select13[rel] = A -> C
}
assert allBCInRel {
select23[rel] = B -> C
}

// rel の濃度がいずれかのシグネチャの濃度と一致するか
assert relCardEqACard {
#A = #rel
}
assert relCardEqBCard {
#B = #rel
}
assert relCardEqCCard {
#C = #rel
}

// rel が存在しないことがあるか
pred noRel { no rel }

検証の結果

先にカッコの有無による挙動差についてだが、
A -> B -> C
と
A -> (B -> C)
では４パターン全てで同じ結果となった。
このため、デフォルトでは多重度キーワードは右結合で扱われるもののようである。
集合Aと関係B -> C の関係の多重度と、集合Bと集合Cの関係の多重度、というように入れ子で扱われているということのようである（p263の記述参照）。

以下、各パターン毎の結果について。

//rel in A one -> B -> C
//rel in A one -> (B -> C)
//rel in (A one -> B) -> C

これは、B -> C の全ての組について A が関数的、となった。
existsAloneA, allBCInRel が成り立つ。
また、カッコありの場合、どちらのパターンでも、カッコなしの場合と同じ結果となった。

//rel in A -> one B -> C
//rel in A -> one (B -> C)

これは、全ての A について B -> C が関数的、となった。
existsAloneB, existsAloneC, relCardEqACard が成り立つ。

//rel in (A -> one B) -> C

これは、A -> C の全ての組について B が関数的、となった。
existsAloneB, allACInRel が成り立つ。

//rel in A -> B one -> C
//rel in A -> (B one -> C)

これは、A -> C の全ての組について B が関数的、となった。
existsAloneB, allACInRel が成り立つ。
(A -> one B) -> C と同じ。

//rel in (A -> B) one -> C

これは、全ての C について B -> C が関数的、となった。
existsAloneA, existsAloneB, relCardEqCCard が成り立つ。

//rel in A -> B -> one C
//rel in A -> (B -> one C)

これは、A -> B の全ての組について C が関数的、となった。
existsAloneC, allABInRel が成り立つ。

//rel in (A -> B) -> one C

このパターンは少々特殊？で、
existsAloneA, existsAloneB, existsAloneC が全て成り立った。
つまり、noRel が成り立った。

これまでの流れからすれば、A -> B の全ての組について C が関数的、になりそうに見えるが、実際にはそうなっていない。
推測するに、矢印演算子の左辺が集合の場合と関係の場合で挙動が異なる、ということだろうか。

p263の記述で、

r: e1 m -> n (e2 m' -> n' e3)

という多重度制約は、e1 が集合の場合は、

all x: e1 | x.r in e2 m' -> n' e3

と、e1 が関係の場合は、

all x, y:univ | x->y in e1 implies y.(x.r) in e2 m' -> n' e3

と等価であると書かれている。
矢印の左辺が関係の場合は、imply に展開されるので、no x->y の場合はこの後の多重度指定が無視される、ということか。
(A -> B) one -> C の場合は、C から A -> B へのone制約があるので、no A -> B は成立し得ない。

考察

以上、とりあえず、one が１回出現するパターンについて確認した。

カッコの規則が確認できたのは収穫だったと思う。
後は、矢印を挟んで one と同じ側にある項が、残り２つの項の直積に対して１個、という感じでイメージしておけばよさそうである。

ちょっと面白いのは、
A -> one (B -> C)
(A -> B) one -> C
のような、あるシグネチャの集合に対して２項関係が１個、という指定が B については行えない、という点である。
要するに、A と C を直接つなぐ矢印が上記の記法では書けないからなわけであるが。
逆に、A -> C について B が１個、という書き方が複数あることになっている。

で、Time イディオムを使う場合。

静的なモデルで「あるAについてBが一つ決まる」とする場合は、以下となるが、

sig B {}
sig A {
rel : one B
}

これを動的なモデルとする場合は、こうすればよさそうである。
（というか、ホテルの客室施錠の例等でこの書き方が使われている）

sig Time {}
sig B {}
sig A {
rel : B one -> Time
}

この場合は、「あるAとTimeの組についてBが一つ決まる」となる。
ただし、この宣言が、rel にはAとTimeの組が全て含まれる、ことも含意している点には注意がいる。
all t : Time | all a : A | one a.rel.t
となる。
このモデル上では、ある Time について、ある A が rel 上にないことがない。
ただ、この点を把握した上で使う分にはさほど不自由はないと思われる。

lone の場合の挙動は上記の one の場合から類推可能と思われる。
some の場合は、もしかしたら挙動が想定と変わってくるかもしれない。
多重度キーワードが複数出るケースは、あまり考えたくない。

諸々見た感想としては、やはり３項関係は可能な限り避けたい、というところである……。

付記

３項関係についての議論があった模様。中身はまだよく見てない。
Multiplicities in ternary relations - Stack Overflow
http://stackoverflow.com/questions/12501430/multiplicities-in-ternary-relations