在合金中构建关系

Question

在哲学家就餐问题中，我们有一张哲学家和叉子的桌子。

sig P {}
sig F {}

对于这个问题，我想要代表表格的以下关系：

P1 -> F1
F1 -> P2
P2 -> F2
F2 -> P3
P3 -> F3
F3 -> P1

即每个 P 指向一个 F，每个 F 指向一个 P，这将形成一个圆。我想调用一个函数来获得这种关系：

fun table : (P+F) one -> one (P+F) { ... }         

我一直在努力完成这项工作，但感觉就像我错过了一些与我遇到的其他问题相关的基本内容。不知何故，我想念一个“构造函数”。

任何指针？

附加

@Hovercouch 通过帮助器sig 提供了一个可行的解决方案。但是，这需要对 P 和 F 进行非自然扩展，并引入了新的 sig。这也可以通过以下方式解决：

sig P, F {}
one sig Table {
    setting : (P+F) one -> one (P+F)
} {
    # P = # F
    all p : P, f : F | P in p.^setting and F in f.^setting
}
run {} for 6

解决了非自然继承问题。

但是，对于一个非常简单的问题，它似乎仍然非常全球性和大量工作。仍然保持问题开放，看看是否有其他解决方案。

Answer 1

这里可能需要在表现力和易处理性之间进行设计权衡。

肯定存在什么是干净或直观的问题；您说 P 和 F 的“下一个”是“表格设置的一个方面”而不是“P 或 F 的一个方面”。我想我理解你的想法，但我认为你不太可能更成功地定义一种原则方法来区分 P 和 F 的“方面”以及它们出现在其域或范围内的关系，而不是任何在过去的几千年里，那些试图可靠地区分本质和偶然性的哲学家。

如果我们接受这种区别是不可靠的，但我们仍然认为它有用，那么问题就变成了“谁制定了这样的规则，即定义为签名的一部分的关系必须与所涉及的个人的（内在）方面相关，而不是不是个人的一个方面的外在关系？”答案是：你做到了，而不是合金的[创造者]。如果一个人过于强烈地坚持自己对想要用来表达某事的构念的直觉，那么就有一定的风险，即不仅坚持该事物应该是可表达的，而且我们应该能够使用特定的构念来表达它。这种坚持可以教会我们很多关于符号的知识，但有时更容易接受符号的设计者也有直觉。

Daniel Jackson 的 Software Abstractions 中的问题Does Alloy 允许独立声明吗？ 中讨论了这个一般性主题（在关于高阶量化的第 3.5.3 节之后的讨论中） 必须将所有关系声明为字段吗？（在第 4.2.2 节关于基本字段声明的讨论中）。讨论的核心是“如果你想声明一些自然不属于任何现有签名的关系，你可以简单地将它们声明为单例签名的字段。” Mutatis mutandis，给出的示例在您的附录中看起来很像 Table sig。

TL;DR 是的，您可能会觉得它有点麻烦，但是包含您不想在其第一个成员上定义的关系的单例 sig 确实与现有的惯用语一样接近，对于这种类型的东西。

Answer 2

如果您愿意添加辅助对象，我们可以通过创建 abstract sig Thing 然后创建 Thing 的 P 和 F 实例来做到这一点：

abstract sig Thing {
    next: Thing
} {
    Thing = this.^@next
}

sig F extends Thing {} {
    next in P
}

sig P extends Thing {} {
    next in F
}

fact SameNumberOfThings {
    #P = #F
}

run {} for 6