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

Question

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

例如，在下面的代码中，我想将 ref 定义为 QArrow 和事件之间的双射。因此，我写了事实bij。但是合金抱怨，因为我认为我量化了使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

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

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 和关系事件之间的双射函数。

Answer 2

也可以将

量化变量的域还原到它们相应的范围，如波纹管：(对于类型为 QArrow 的元素，将univ更改为 QArrow，对于打算处于event关系中的元素对，将univ->univ更改为State ->State。

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
}