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
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]
ando in B[o]
should raise a type error, since if A and B are predicates, then the expressionsA[o]
andB[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
And if you want an exclusive disjunction -- I assume that this is what you mean when you speak of a disjoint union -- then
If you want the sets for which A, B, and X are true, then you want to write
The third of these can of course be written
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:
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:
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:
PS: we assume that we have
sig Object {}
in our signature.