(I'm not sure I have the correct words for this, so bear with me if this seems fuzzy.)
Bear in mind that all expressions in Alloy that denote individuals denote sets of individuals, and that there is no distinction available in the language between 'individual X' and 'the singleton set whose member is the individual X'. ([Later addendum:] In the terms more usually used: the general rule in Alloy's logic is that all values are relations. Binary relations are sets of pairs, n-ary relations sets of n-tuples, sets are unary relations, and scalars are singleton sets. See the discussion in sec. 3.2.2 of Software Abstractions, or the slide "Everything's a relation" in the Alloy Analyzer 4 tutorial by Greg Dennis and Rob Seater.)
Given the declaration you give of the 'show' predicate, it's easy to expect that the argument of 'show' should be a single Book -- or more correctly, a singleton set of Book --, and then to expect further that if the argument is not actually a singleton set (as in the expression show[Book]
here) then the system will coerce it to being a singleton set, or interpret it with some sort of implicit existential or universal quantification. But in the declaration pred show(b:Book) ...
, the expression b:Book
just names an object b which will be a set of objects in the signature Book. (To require that b be a singleton set, write pred show(one b: Book) ...
.) The expression which constitutes the body of show
is evaluated for b = Book just as readily as for b = Book$0.
The appearance of existential quantification is a consequence of the way the dot operator at the heart of the expression addr[b,n]
(or equivalently n.(b.addr)
is defined. Actually, if you experiment you'll find that show[Book] is true whenever there is any name for which the set of all books contains a mapping to two different addresses, even in cases where an existential interpretation would fail. Try adding this to your model, for example:
pred hmmmm { show[Book] and no b: Book | show[b] }
run hmmmm for exactly 2 Book, exactly 2 Addr, exactly 2 Name