Несвязный союз и декартово произведение в сплаве

Question

У меня есть два набора предикатов понимания (униатных), как показано ниже в Alloy:

pred A (o : Object){ .. } 

pred B (o : Object) { ..} 

Я хотел бы определить предикаты, один из которых является несвязным объединением, а другой - декартовым произведением A и B.

PS: чтобы определить их объединение и пересечение, я могу определить следующий предикат:

pred Union(o : Object){
    A[o] or B[o]
}

pred Inter(o:Object){
  A[o] and B[o]
}

Я хотел бы получить аналогичные предикаты для декартового произведения и непересекающегося объединения.

Спасибо

Answer 1

Вы можете смешивать понятия предикатов и понятия множеств. У вас хорошая компания (например, Фреге), но она оказывается опасной.

Выражения o in A[o] а также o in B[o] должно вызвать ошибку типа, так как если A и B являются предикатами, то выражения A[o] а также B[o] следует оценивать как истинное или ложное, а не как наборы, в которые o мог бы входить член.

Если вы хотите предикат U, который является истинным для объекта, когда либо A, либо B, либо оба являются истинными для этого объекта, то вам нужно что-то вроде

pred U[o : Object] { A[o] or B[o] }

И если вы хотите исключить дизъюнкцию - я предполагаю, что именно это вы имеете в виду, когда говорите о непересекающемся союзе - тогда

pred X[o : Object] { (A[o] and not B[o]) or (B[o] and not A[o]) }

Если вы хотите, чтобы множества, для которых A, B и X истинны, то вы хотите написать

{ o : Object | A[o] } 
{ o : Object | B[o] } 
{ o : Object | X[o] } 

Третий из них, конечно, может быть написан

{ o : Object | (A[o] and not B[o]) or (B[o] and not A[o]) }

Обозначение понимания набора (опять же, я рекомендую вам прочитать соответствующую документацию) также может обрабатывать наборы кортежей; декартово произведение множеств объектов, удовлетворяющих A и B, будет записано так:

{ a, b : Object | A[a] and B[b] }

Answer 2

Вот решение того, что я искал:

Декартово произведение A и B определяется как A * B = {(a,b) | a в A и b в B}. Таким образом, помещение его в синтаксис Alloy с заданным выражением понимания будет следующим:

pred ACartesB(o1:Object, o2: Object){
    A[o1] and B[o2]
}

непересекающиеся объединения A и B определяются как A+B= {(a,1) union (b,2) | a в A и b в B}. 1 и 2 являются индексами для различения одинаковых элементов A и B в A+B. Таким образом, поместить его в контекст сплава можно следующим образом:

pred AdisjUnionB(o:Object, i: Int){
    (A[o] and i=1) or (B[o] and i=2)
}

PS: мы предполагаем, что у нас есть sig Object {} в нашей подписи.