Сплав - решение парадокса Барбера все еще противоречиво

Известно, что парадокс парикмахера решается, если есть несколько парикмахеров, чтобы они могли брить друг друга.

Эта спецификация соответствует:

 sig Man {shaves: set Man} 
 some sig Barber extends Man {} 
 fact {   
   Barber.shaves = {m: Man | m not in m.shaves} 
 } 
 run { } for 4

Однако следующее, хотя и выглядит эквивалентным, все же несовместимо:

sig Man {
 shavedMen : set Man
}
fact {
 # {barber:Man | barber.shavedMen = {m: Man | m not in m.shavedMen} } > 1
}
run {} for 4

Почему?


logic alloy
person user3900775    schedule 17.11.2014    source источник

Ответы (1)


arrow_upward
4
arrow_downward

В первом факте вы настаиваете: множество мужчин, которых бреют все парикмахеры, — это все мужчины, которые не бреются сами.

Редактировать моему объяснению второго факта явно недоставало ясности. Вы утверждаете, что человек считается брадобреем, если множество мужчин, которых он бреет, равно множеству всех мужчин, которые не бреются (включая его, отсюда и несоответствие, и в этом вся прелесть этой проблемы).

person Loïc Gammaitoni    schedule 17.11.2014
comment
Я понимаю. Так почему второй несовместим? - person user3900775; 18.11.2014
comment
Спасибо, Лоик! Во втором я утверждаю, что парикмахеров больше одного (крайний оператор на самом деле — ›). Это должно было сделать спецификацию согласованной (как в первом случае), но этого не произошло. Любая подсказка, почему? - person user3900775; 20.11.2014