Преобразование выражения высшего порядка в логику первого порядка сплава

Я хотел бы написать взаимно однозначное соответствие между набором и отношением в Alloy.

Например, в следующем коде я хотел бы определить ref как соответствие между QArrow и событием. Поэтому пишу факт 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, а когда мы не можем этого делать?

Спасибо


logic first-order-logic alloy
person qartal    schedule 17.12.2014    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Вот решение этой проблемы (я разместил вопрос в математической нотации в разделе math satck exchange здесь и получил решение) конвертирую на 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
}

В приведенном выше коде этот факт требует, чтобы ref была взаимно однозначной функцией между QArrow и событием отношения.

person qartal    schedule 18.12.2014

arrow_upward
0
arrow_downward

Также возможно ограничить область количественных переменных до их соответствующей области, как показано ниже: (изменение 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

}
person qartal    schedule 18.12.2014