在 Daniel Jakson 所著的 Alloy 名著中，他描述了在 Alloy 中指定约束的三种不同风格：1）谓词演算、2）导航风格和 3）关系演算。（第 3.1 节，第 34 页）
对我来说，第一个和最后一个背后的理论在某种程度上是清楚的，因为当我们将关系作为谓词时，第一个是传统的一阶逻辑；最后是关系演算，其中一切都被视为关系，并通过使用方程符号和一些代数运算（没有量词）来指定约束。书中说第二个最具表现力（第35页）。
我的问题： 第二个（即导航风格）背后的理论是什么？我应该在哪里寻找（以及在哪些术语下）以获得有关这一问题的更多理论上的信息。
导航风格的动机是你想要介于谓词演算和关系演算之间的东西，谓词演算没有对集合或关系的操作，因此在实践中使用起来非常尴尬和冗长（并且由于缺乏传递闭包而表达能力较差）。微积分，由塔斯基（Tarski）开创，它为您提供关系运算符，但没有量词，这对大多数人来说非常不自然（但它允许一些精美简洁的方式来表达属性）。导航风格介于两者之间，并为您提供了集合/关系运算符和量词，因此从这个意义上说 - 至少是非正式的，如果您仔细定义了这三种子语言，也可能是正式的 - 它比任何一种都更具表现力。同时，我想到大多数人对简单的一阶量词感到满意，但对关系连接不太满意，因此倾向于编写其中表达式表示集合的公式。您可以将这些表达式中的每一个视为从某个原子开始，由量化变量表示，然后沿着关系“导航”以获得表示原子集的越来越大的表达式。这就是我对像 me.parents.children 这样的表达式的看法：从我开始，导航到我的父母，然后从他们到他们的孩子——结果是包含我和我的兄弟姐妹的集合。根据我的经验，这种导航风格是大多数人自然倾向于的。
确实，如果您必须从与 OCL 匹配的三种样式中选择一种，那就是这种导航样式，尽管 OCL 确实具有非常复杂的语义（由于每一步都会自动发生各种强制和扁平化） ，其中 Alloy 中的语义只是标准集和关系。语法可能更多地受到 Java 等面向对象语言的影响，尽管它们没有 Alloy 所具有的那种关系图像（也就是说，如果你有一个字段 f 并且可以写 xf，则不能写 xs。 f 表示由 f 从集合 xs 中的对象映射到的所有对象的集合！）。但请注意，这里没有特殊的语法；这些只是相同运算符的使用方式。
当我在书中写下这一页时，我认为这会给读者一些有用的直觉，但它似乎只是造成了更多的混乱！