Multiplicities in ternary relations

Question

The semantics of the lower-bound multiplicities some and one in ternary relations are hard to grasp. According to Software Abstractions (Rev. ed.) pp.79-80 the relation addr: Book -> (Name -> some Addr) should be equivalent to all b: Book | b.addr in Name -> some Addr (see also p.97). But what does the latter formula exactly mean? My imagination fails here. That's why I did some experiments in the Alloy Analyser 4.1.0. The implication in this model:

sig Name, Addr {}
sig Book { addr: Name -> some Addr }
assert implication {
 #Book = 0 or all n: Name | some b: Book, a: Addr | n in b.addr.a
}
check implication

holds (no counterexample found). So if there is any Book, each Name should be registered in at least one of those Books. Undocumented Addrs are allowed, and without Books, undocumented Names suddenly appear to be allowed too.

The implication in the following model:

sig Name, Addr {}
sig Book { addr: Name some -> Addr }
assert implication {
  #Book = 0 or all a: Addr | some b: Book | #b.addr.a > 0
}
check implication

holds again. It's the mirror image of the previous model: undocumented Addrs are forbidden, unless there is no Book at all. And there are no constraints with respect to the documentation of Names.

Both models can be combined and formulated more concise:

sig Name, Addr {}
sig Book { addr1: Name -> some Addr, addr2: Name some -> Addr }
assert implications {
  some Book implies Name in Book.addr1.Addr and Addr in Book.addr2[Name]
}
check implications

So if there is any Book, all Names should participate in the relation addr1 and all Addrs should participate in addr2. The multiplicity one behaves alike.

It seems Software Abstractions and the Analyser don't tell the same story about constructs like R: A -> (B m -> n C) as far as lower-bound constraints are concerned, but I may have missed something. The implications I found were not what I had expected, and there may be other weird implications that I haven't discovered yet. More and more I feel that nested lower-bound multiplicities make no sense at all. Could I be right on this?

Answer 1

The first example puzzled me for a long while; it surprised me that no unmapped names were present in any instances. For what it's worth, however, I find on p. 78 of the first edition the statement that "Multiplicities are just a shorthand, and can be replaced by standard constraints; the multiplicity constraint in

r: A m -> n B

can be written as

all a: A | n a.r
all b: B | m r.b

Applying the first of these rewrite rules to the statement

all b: Book | b.addr in Name -> some Addr

which you derive from the first example model, we get

all b: Book | all n: Name | some n.(b.addr)

or in prose "for all books b and names n, there is some mapping for n in b.addr", which at least addresses my initial puzzlement. To allow unmapped names one must write either sig Book { addr: set (Name -> Addr) } or (as in the later examples in the Whirlwind Tour) sig Book { names: set Name, addr: names -> some Addr}.

I have had a little more trouble with the second rewrite rule (the one involving m). There is no explicit multiplicity on Name (no m), and I spent some time looking through the book to find a specification of the default multiplicity constraint on relations (analogous to the default one for other fields), and experimenting with various ways of writing equivalent constraints, before concluding that there is no default multiplicity constraint; instead, the default is that there is no multiplicity constraint. So the second rewrite rule given on p. 78 does not apply to Name -> some Addr; there is no multiplicity constraint, and the effect is that for each a in Addr, there may be zero or more instances of (b.addr).a.

I guess from a language-design point of view, I think it might help to have an explicit "default multiplicity constraint" of set and to allow statements like

all b: Book | all a: Addr | set (b.addr).a
/* currently produces type error */

with the meaning that there may be zero or more entries in b.addr for each address.

But I am inclined to think that with or without such a change you will still be right to say that the effects of some and one in ternary relations can be hard to grasp.