Higher-order quantification could not be skolemized

Questions
1

Suppose we have the following simple model:

sig User {}

sig Group {
  users: set User
}

Is it possible to use Alloy to find a relation over users that isn’t explicitly defined in the model?

For example:

check {
  some r: User -> User | some disj u0, u1: User | u1 in u0.^r
}

Basically, “does there exist a relation over users such that u0 can reach u1?” I would expect the analyzer to tell me that users can be related through a common Group.

I have tried this assertion but I get the error: Analysis cannot be performed since it requires higher-order quantification that could not be skolemized. I tried changing the solver but that didn’t work.

Is there another way to discover this relation with Alloy?

If so, would it be possible with n-arity relations? Suppose …

sig User {}

sig Group {
  users: set User
}

sig MetaGroup {
  groups: set Group
}

Now users could be related by common Group or common MetaGroup.

Is it possible to consider User -> User and User -> univ -> ... -> univ -> User within a bounded scope?

2

A limited form of higher-order quantification is indeed possible. Quoting an example by @aleks et al:

sig Node { key: one Int }

pred clique[edges: Node->Node, clqNodes: set Node] {
	all disj n1, n2: clqNodes | n1->n2 in edges
}

run {
	some edges: Node -> Node |
	some clqNodes: set Node |
	clique[edges, clqNodes]
}

Observe higher order quantification both on edges and clqNodes.

Why is the run allowed? Because these variables can be Skolemized as they are quantified existentially. Which roughly means that the spec if morally equivalent to one when the user would have added constants representing the existentially-quantified variables. Notice that existential quantifiers can appear under universal ones up to a certain point ans still be Skolemized, depending on the value of the Skolem depth option.

OTOH universal higher-order quantification cannot be Skolemized so it’s forbidden. Notice that a check is more or less like a run with a negation added to the front. So existentially-quantified variables in a check will turn universal (for the same reason, universal quantifiers in a check will turn existential so will be Skolemizable). This is why your check fails.

@aleks had developed Alloy*, a higher-order version of Alloy 4, but it’s not integrated into Alloy.