alloy formula, expressing foreach operation

Question

I am an alloy new user and I am trying to declare in a predicate that

There is a y in Y for each x in X

but when I write it this way :

all x : X | all y : Y | one y

all x : X | all y : Y | one x => one y

I have only one y for the whole X

What I expect is if there is 3 x there will be 3 y. I not want to use cardinality comparison because I try to model morphisms.

Can someone help me?

thanks in advance.

Answer 1

You should take user1513683's answer and have f be a field in a sig, as opposed to using it as a quantification variable, e.g.,

sig X {}
sig Y {}
one sig M {
  f: X one -> one Y
}
run {} for 4

As you already realized, you could avoid introducing a new sig and embed this constraint in an existential quantifier, e.g.,

run {
  some f: X one -> one Y | 1=1
} for 4

The reason why you can here use an existential quantifier over a binary relation is the underlying constraint solving mechanism. If the goal is to find just one instance of a binary relation (existential quantification) for which the quantifier's body holds true, that's much easier than asking whether the body holds true for all possible instances of a binary relation (universal quantification). For the former case, the quantifier can be skolemized, i.e., replaced with a number of free variables, and then the solver is asked to find any solution (a set of values for those variables) such that the body holds; that process is simply not possible when the goal is to check the body for all possible solutions.

Answer 2

Y=#X says that there are the same number of Ys as Xs.

Or do you mean #X=<#Y ? There is a y in Y for each x in X, and possibly some spare Ys.

Or do you need a name for the connection? In which case, introduce

f : X one->one Y // exactly one-one or f : X lone->one Y // every X has exactly one Y, but a Y has at most one X

in an appropriate signature.