不能被分解的高阶量化

Question

我正在学习 Alloy 并尝试为关系 injective 和 surjective 创建谓词。我在 Alloy 中尝试使用以下模型：


sig A {}
sig B {}

pred injective(r: A -> B) {
    all disj a, a': r.B | no (a.r & a'.r)
}

pred inj {
    no r: A -> B | injective[r]
}

run inj for 8

但是，我在 no r 上收到此错误：

Analysis cannot be performed since it requires higher-order quantification that could not be skolemized.

我已经阅读了有关 skolemization 的软件抽象部分和其他一些 SO 问题，但我不清楚这里的问题是什么。我可以通过重新措辞来解决这个问题还是遇到了基本限制？

编辑：

经过一些试验，这个问题似乎与否定有关。要求 some r: A -> B | injective[r] 立即产生一个内射的例子。作为一个通常更难的问题，这在概念上是有意义的，但它们在小范围内似乎或多或少是同构问题。

编辑 2：

我发现使用以下模型 Alloy 给我的示例也满足给我错误的注释谓词。


sig A {}
sig B {}

pred injective(r: A -> B) {
    all disj a, a': r.B | no (a.r & a'.r)
}

pred surjective(r: A -> B) {
    B = A.r
}

pred function(f: A -> B) {
    all a: f.B | one a.f
}

pred inj {
    some s: A -> B | function[s] && surjective[s]
    // no r: A -> B | function[r] && injective[r]
}

run inj for 8

Answer 1

可以这样想：每个 Alloy 分析都涉及模型查找，其中解决方案是将名称映射到关系的模型（在 Alloy 中称为实例）。要显示公式根本不存在模型，您可以运行它，如果 Alloy 找不到解决方案，则不存在模型（在该范围内）。所以如果你运行

some s: A -> B | function[s] && surjective[s]

你得不到解决方案，你知道在那个范围内没有满射函数。

但是，如果您要求 Alloy 找到一个与该模型不存在任何关系的模型，那就是一个非常不同的问题，需要更高阶的分析，因为求解器不能只找到一个解决方案：它需要证明没有满足否定约束的解决方案的扩展。你最初的例子就是这样。

所以，是的，从根本上说，高阶逻辑不太容易处理，这是一个基本限制。但这在实践中是否对您有限制是另一回事。您实际需要什么分析？

高阶公式的一个引人注目的用途是合成。一个典型的综合问题采用 "find me a program structure P such that there is no counterexample to the specification S" 的形式。这需要更高阶的分析，也是 Alloy* 旨在解决的问题。

但通常没有理由使用 Alloy* 来解决标准 verification/simulation 问题。

不能被分解的高阶量化

higher-order quantification that cannot be skolemized

alloy