higher-order quantification that cannot be skolemized

Question

I'm learning Alloy and experimenting with creating predicates for relations being injective and surjective. I tried this in Alloy using the following model:


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

However, I get this error on no r:

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

I've read the portions of Software Abstractions about skolemization and some other SO questions but it's not clear to me what the issue is here. Can I fix this by rephrasing or have I hit a fundamental limitation?

EDIT:

After some experimenting the issue seems to be associated with the negation. Asking for some r: A -> B | injective[r] immediately produces an injective example. This makes conceptual sense as a generally harder problem, but they seem like more or less isomorphic questions in a small scope.

EDIT2:

I've found using the following model that Alloy gives me examples which also satisfy the commented predicate that gives me the error.


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

Daniel Jackson Daniel Jackson · Accepted Answer · 2018-12-20T12:41:33

Think of it like this: every Alloy analysis involves model finding, in which the solution is a model (called an instance in Alloy) that maps names to relations. To show that no model exists at all for a formula, you can run it and if Alloy finds no solution, then there is no model (in that scope). So if you run

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

and you get no solution, you know there is no surjective function in that scope.

But if you ask Alloy to find a model such that no relation exists with respect to that model, that's a very different question, and requires a higher order analysis, because the solver can't just find a solution: it needs to show that there is no extension of that solution satisfying the negated constraint. Your initial example is like that.

So, yes, it's a fundamental limitation in the sense that higher order logic is fundamentally less tractable. But whether that's a limitation for you in practice is another matter. What analysis do you actually need?

One compelling use of higher order formulas is synthesis. A typical synthesis problem takes the form "find me a program structure P such that there is no counterexample to the specification S". This requires higher order analysis, and is the kind of problem that Alloy* was designed to solve.

But there's generally no reason to use Alloy* for standard verification/simulation problems.

higher-order quantification that cannot be skolemized

1 Answers