alloy - Barber Paradox 为什么这个模型不一致？

Question

我想知道为什么这个模型不一致？我们可以在 shaves 中有以下元组。

shaves = {(man,man)} sig Man {shaves: set Man} one sig Barber extends Man {}

fact {
   Barber.shaves = (m:Man |m not in m.shaves}
}

Barber.shaves 将产生 0 个元组。在这种情况下，事实应该是有效的。那么为什么允许告诉我我的模型不一致？

非常感谢对此的一些建议。

Answer 1

好的，这是解决方案。这个想法很简单，我认为作者真的应该在他们的书中解释这一点。

混淆的症结在于事实陈述。

Barber.shaves = {m:Man | m 不在 m.shaves}

基本上，上述声明的意思是，Barber.shaves 中的任何元组都不能自己刮胡子。例如 = Barber.shaves = {(m)}，则(m, m)绝不能出现在剃须关系集中。此外，m:Man 表示每个不刮胡子的人也应该在 Barber.shaves 中。

当我们来到 Barber 实例时，问题就出现了。如果 barber 不在 Barber.shaves 中，则违反 m : Man。如果 barber 包含在内，则它违反 m not in m.shaves 因为 shaves 将包含 {(barber, barber)}

我希望这可以消除像我这样的合金初学者的困惑。

因此，鉴于我问题中的当前模型，合金无法创建满足这一事实的实例。

Answer 2

有一个仅使用英语的简单解释。

上面的合金事实表明，理发师（只有一个理发师，因为one sig Barber）剃须的一组男士与所有不刮胡子的男士完全相等。起初，这种说法是有道理的，因为每个人要么自己刮胡子，要么被理发师刮胡子。

诀窍问题是“谁给理发师刮胡子”。如果理发师不给自己刮胡子，那么这个事实就会迫使理发师必须给理发师刮胡子，这与理发师不给自己刮胡子的假设相矛盾。如果理发师自己刮胡子，那么理发师一定不能给理发师刮胡子，这又是一个悖论，所以找不到例子。