如何阅读顺序声明？

Question

在附录 B：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

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

我的尝试是“如果有一个实例，即由 X 中的一个 x 和 Y 中的一个 y 组成，且 F 为真，则这是真的”。

Answer 1

直观地说，one x: X, y: Y | F 的意思是“在 XxY s.t. F 中恰好有一对 (x,y)”，而 one x: X | one y: Y | F 的意思是“在 X s.t 中恰好有一个 x：在 Y s.t. F 中恰好有一个 y ”。在后一种情况下，唯一的 y s.t. F 可能取决于给定的 x。

要查看正式发生的情况，您可以将one 翻译成all 和some；然后以这种方式重铸你的例子。