logic - 将高阶表达式转换为合金一阶逻辑

Question

我想在合金中写一个集合和一个关系之间的双射。

例如，在下面的代码中，我想将 ref 定义为 QArow 和 event 之间的双射。因此，我写了事实bij。但是 Alloy 抱怨说，因为我认为我量化了使bij事实中的两个表达式成为高阶逻辑表达式的关系：

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
}

如何将这些表达式转换为一阶逻辑表达式？

另外，一般来说，当我们可以将 HOL 表达式转换为 FOL 表达式以及何时不能这样做时，是否有任何指导方针？

谢谢

Answer 1

univ也可以将量化变量的域限制在它们相应的范围QArrow内QArrow，univ->univ如下State ->State所示event：

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

}

Answer 2

这是这个问题的解决方案（我在这里的数学 satck 交换中以数学符号发布了问题并得到了解决方案）我正在将其转换为合金。

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
}

在上面的代码中，事实将ref强加为QArrow和关系event之间的双射函数。