构建合金关系

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

如果你愿意添加一个辅助对象，我们可以通过制作一个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

Answer 2

这里涉及设计权衡，表达能力和易处理性之间。

当然存在一个干净或直观的问题;你说P和F的'下一个'是“表设置的一个方面”而不是“P或F的一个方面”。我想我理解你的想法，但我不认为你有可能更成功地定义一种原则性的方法来区分P和F的“方面”以及它们出现的领域或范围内的关系，不仅仅是任何一个在过去的几千年里，曾经尝试过在实质和事实之间进行可靠区分的哲学家们。

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

在Daniel Jackson的软件抽象中，在合金允许独立声明的问题下讨论了这个一般性主题吗？ （在关于高阶量化的第3.5.3节的讨论中）并且必须将所有关系声明为字段？ （在关于基本字段声明的4.2.2节之后的讨论中）。讨论的核心是“如果你想声明一些不属于任何现有签名的关系，你可以简单地将它们声明为单一签名的字段。”经过必要的修改后，给出的例子在您的附录中看到了很多表格。

TL; DR是的，您可能会发现它有点麻烦，但是包含您不想在其第一个成员上定义的关系的单例符号实际上与这样的事物一样接近已建立的惯用语。