Как вывести ограничение множественности «один» с помощью языка ядра Alloy?

Question

Я читал Приложение C: Семантика ядра к книге Software Abstraction (Дэниел Джексон, второе издание, очень приятно читать, кстати!) И обнаружил, что немного застрял в понимании того, как вывести ограничение множественности one, используя другие конструкции ядра.

Я понимаю, что no может быть получено с использованием expr = none, а some может быть получено с использованием отрицания предыдущего правила, но я не понимаю, как express ограничение one (и, следовательно, lone) с использованием только конструкций ядра (или производных).

Возможно, мне не хватает чего-то очевидного, но я этого не вижу :)

Answer 1

Вы можете определить one следующим образом:

one e iff
not all x: e | not x = x // e is non-empty
and
all x: e | all x': e | x = x' // e has no more than one member

Обратите внимание, что языка ядра недостаточно для express количественных оценок более высокого порядка (которые поддерживаются Alloy *, но не очень эффективно самим Alloy ). Таким образом, квантификатор дает нам понятие синглтона.

Daniel

Answer 2

Вот как бы я express one expr

//there is some expr
not (expr = none)
//and all expr should be one and the same because there's only one expr. 
all x1,x2: expr | x1=x2