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?

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.