如何阅读顺序声明？

Question

在附录 B：Alloy Software Abstractions 的语言参考中指出

all x: X, y: Y | F

是

的缩写

all x: X | all y: Y | F 

但是

one x: X, y: Y | F 

不是

的缩写

one x: X | one y: Y | F

我不太清楚这里发生了什么，我突然想到我可能根本没有正确阅读它..

我的尝试是 "this is true if there is one instance, comprised of one x from X and one y from Y for which F is true"。

Answer 1

直觉上，one x: X, y: Y | F 表示 "there is exactly one pair (x,y) in XxY s.t. F"，而 one x: X | one y: Y | F 表示 "there is exactly one x in X s.t: there is exactly one y in Y s.t. F"。在后一种情况下，唯一的 y s.t。 F 可能取决于给定的 x.

要正式了解会发生什么，您可以将 one 翻译成 all 和 some；然后以这种方式重铸您的示例。