disjoint union and Cartesian product in Alloy

问题:

I have two set comprehension predicates (uniary) as bellow in Alloy:

pred A (o : Object){ .. } 

pred B (o : Object) { ..} 

I would like to define predicates, one of which is disjoint union and another one is Cartesian product of A and B.

PS: To define their union and intersection I can define the following predicate:

pred Union(o : Object){
    A[o] or B[o]
}

pred Inter(o:Object){
  A[o] and B[o]
}

I would like to get similar predicates for Cartesian product and disjoint union.

Thanks

回答1:

You may be conflating the concepts of predicates and the concepts of sets. You have good company (Frege, for one), but it turns out to be dangerous.

The expressions o in A[o] and o in B[o] should raise a type error, since if A and B are predicates, then the expressions A[o] and B[o] should evaluate to true or false, and not to sets of which o could conceivably be a member.

If you want a predicate U which is true of an object when either A or B or both are true for that object, then you want something like

pred U[o : Object] { A[o] or B[o] }

And if you want an exclusive disjunction -- I assume that this is what you mean when you speak of a disjoint union -- then

pred X[o : Object] { (A[o] and not B[o]) or (B[o] and not A[o]) }

If you want the sets for which A, B, and X are true, then you want to write

{ o : Object | A[o] } 
{ o : Object | B[o] } 
{ o : Object | X[o] } 

The third of these can of course be written

{ o : Object | (A[o] and not B[o]) or (B[o] and not A[o]) }

The set comprehension notation (again, I encourage you to read the relevant documentation) can also handle sets of tuples; the Cartesian product of the sets of objects satisfying A and B would be written this way:

{ a, b : Object | A[a] and B[b] }

回答2:

Here is the solution to what I was looking for:

cartesian product of A and B are defined as A * B = {(a,b) | a in A and b in B}. So putting it in Alloy syntax with set comprehension expression would be as follows:

pred ACartesB(o1:Object, o2: Object){
    A[o1] and B[o2]
}

disjoint union of A and B are defined as A+B= {(a,1) union (b,2) | a in A and b in B}. 1 and 2 are indexes to distinguish the same elements of A and B in A+B. So putting it in alloy context would be as the following:

pred AdisjUnionB(o:Object, i: Int){
    (A[o] and i=1) or (B[o] and i=2)
}

PS: we assume that we have sig Object {} in our signature.