несвязное объединение и декартово произведение в сплаве

У меня есть два набора предикатов понимания (униарных), как показано ниже в 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]
}

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

Спасибо


alloy
person qartal    schedule 06.12.2014    source источник

Ответы (2)


arrow_upward
2
arrow_downward

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

Выражения 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] }
person C. M. Sperberg-McQueen    schedule 06.12.2014
comment
Я поправил органы Союза и Интера. Есть причина, по которой я рассматривал наборы как унарные предикаты в своем приложении. А как насчет несвязного объединения двух множеств и декартова произведения? как я могу написать их как предикаты? - person qartal; 06.12.2014
comment
@qartal, если под «непересекающимся союзом» вы подразумеваете что-то иное, чем исключительная дизъюнкция, описанная в ответе, то вам, вероятно, нужно определить, что вы имеете в виду. Декартовы произведения также можно выразить с помощью понятий; Я повторяю свою рекомендацию, чтобы вы прочитали о пониманиях в документации. - person C. M. Sperberg-McQueen; 06.12.2014
comment
под непересекающимся объединением я подразумеваю операцию, описанную здесь. не могли бы вы сообщить мне, какой документ вы имеете в виду, чтобы посмотреть на декартово произведение? вы имеете в виду книгу сплавов (программная абстракция)? - person qartal; 06.12.2014
comment
Я не собирался предлагать вам прочитать конкретный отрывок; Software Abstractions действительно обсуждает понимание, и я подозреваю, что учебник по Alloy и справочные материалы в Интернете тоже. Если, прочитав его и рассмотрев приведённые здесь примеры осмыслений, вы не сможете сообразить, как выразить дизъюнктный союз, я очень удивлюсь. - person C. M. Sperberg-McQueen; 06.12.2014

arrow_upward
0
arrow_downward

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

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

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

несвязное объединение A и B определяется как A+B= {(a,1) union (b,2) | а в А и б в В}. 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 {} в нашей подписи.

person qartal    schedule 06.12.2014