formula - 合金公式，表达foreach运算

Question

我是合金新用户，我试图在谓词中声明

There is a y in Y for each x in X

但是当我这样写时：

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

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

我只有一个 y 代表整个 X

我期望的是，如果有 3 x，就会有 3 y。我不想使用基数比较，因为我尝试对态射进行建模。

有人能帮我吗？

提前致谢。

Answer 1

您应该接受 user1513683 的回答并f成为 sig 中的一个字段，而不是将其用作量化变量，例如，

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

正如您已经意识到的那样，您可以避免引入新的 sig 并将此约束嵌入到存在量词中，例如，

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

您可以在这里使用存在量词而不是二元关系的原因是潜在的约束解决机制。如果目标只是找到一个二元关系（存在量化）的实例，而量词的主体对其成立，那比询问主体是否对二元关系的所有可能实例（全称量化）都成立要容易得多。对于前一种情况，量词可以被计算，即用许多自由变量代替，然后求解器被要求找到任何解（这些变量的一组值），使得主体成立；当目标是检查身体是否有所有可能的解决方案时，这个过程根本不可能。

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.