Converting higher order expression into alloy first order logic

Question

I would like to write a bijection between a set and a relation in Alloy.

For example in the following code I would like to define ref to be a bijection between QArrow and event. Therefore, I write the fact bij. But Alloy complains, since I think I quantify over the relations which makes both expressions in the bij fact a higher order logic expression:

sig State {event : set State}
sig QArrow {ref: univ ->univ}

fact bij {
    all q:QArrow | one a: univ->univ | Q[a] and q.ref=a
    all a: univ->univ | one q:QArrow | Q[a] and q.ref=a
}

pred Q (a: univ->univ){
    a in event
}

How to convert these expression to be be first order logic expression?

Also, in general, is there any guideline when we can convert HOL expressions to FOL expression and when we can not do this?

Thanks

Answer 1

Here is the solution to this problem ( I posted the question in mathematical notation in the math satck exchange here and got the solution ) I am converting it to Alloy.

sig State {event : State}
sig QArrow{ref: State -> State}
fact {

        all q:univ | (q in QArrow implies (some s1,s2:univ | ( (s1->s2 in event) 
                            and (q.ref=s1->s2) and some s3,s4:univ | (( (s3->s4 in event) and  (q.ref=s3->s4) ) 
                            implies (s1->s2)=(s3->s4) ))))  // ref is a function

        all q1,q2,s1,s2:univ | (( (q1 in QArrow) and  (q2 in QArrow) and 
                (s1->s2 in event) and (q1.ref=s1->s2) and   (q2.ref=s1->s2)  ) implies q1=q2)   // ref is injective

        all s1,s2:univ | (some q:univ | (  ( s1->s2 in event) implies  
                                                ((q in QArrow) and (q.ref=s1->s2)) )) // ref is surjective
}

In above code the fact imposes ref to be a bijective function between QArrow and relation event.

Answer 2

It is also possible to restric the domain of the quantified variables to their corresponding scope as bellow: (changing univ to QArrow for the elements of type QArrow, and changing univ->univ to State ->State for the pairs intended to be in event relation.

sig QArrow{ref: State -> State}
fact {

        all q:QArrow | (some s1,s2:State | ( (s1->s2 in event) 
                            and (q.ref=s1->s2) and some s3,s4:State | (( (s3->s4 in event) and  (q.ref=s3->s4) ) 
                            implies (s1->s2)=(s3->s4) )))  // ref is a function

        all q1,q2:QArrow, s1,s2:State | ((  (s1->s2 in event) and (q1.ref=s1->s2) and   (q2.ref=s1->s2)  ) implies q1=q2)   // ref is injective

        all s1,s2:State | (some q:QArrow | (  ( s1->s2 in event) implies  
                                                (q.ref=s1->s2) )) // ref is surjective

}