количественная оценка высшего порядка, которую нельзя сколемизировать - PullRequest
Новая
       8

количественная оценка высшего порядка, которую нельзя сколемизировать

0 голосов
/ 15 декабря 2018

Я изучаю Alloy и экспериментирую с созданием предикатов для отношений injective и surjective.Я пробовал это в Alloy, используя следующую модель: 


sig A {}
sig B {}

pred injective(r: A -> B) {
    all disj a, a': r.B | no (a.r & a'.r)
}

pred inj {
    no r: A -> B | injective[r]
}

run inj for 8

Однако я получаю эту ошибку на no r:

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

Я читал части программных абстракций о сколемизации и некоторые другие вопросы SO, но мне не ясно, в чем здесь проблема.Могу ли я исправить это, перефразировав или я столкнулся с фундаментальным ограничением?

РЕДАКТИРОВАТЬ:

После некоторых экспериментов проблема, кажется, связана с отрицанием.Запрос some r: A -> B | injective[r] немедленно приводит к инъективному примеру.Это имеет концептуальный смысл как более сложная проблема, но они кажутся более или менее изоморфными вопросами в небольшом объеме.

EDIT2:

Я обнаружил, используя следующую модель, которую мне дает Alloyпримеры, которые также удовлетворяют прокомментированному предикату, который дает мне ошибку. 


sig A {}
sig B {}

pred injective(r: A -> B) {
    all disj a, a': r.B | no (a.r & a'.r)
}

pred surjective(r: A -> B) {
    B = A.r
}

pred function(f: A -> B) {
    all a: f.B | one a.f
}

pred inj {
    some s: A -> B | function[s] && surjective[s]
    // no r: A -> B | function[r] && injective[r]
}

run inj for 8

1 Ответ

0 голосов
/ 20 декабря 2018

Думайте об этом так: каждый анализ Alloy включает в себя поиск модели, в которой решением является модель (называемая экземпляром в Alloy), которая отображает имена в связи.Чтобы показать, что для формулы вообще не существует модели, вы можете запустить ее, и если Alloy не найдет решения, то модели нет (в этой области).Поэтому, если вы запускаете

some s: A -> B | function[s] && surjective[s]

и не получаете решения, вы знаете, что в этой области нет сюръективной функции.

Но если вы попросите Alloy найти модель, для которой не существует никакого отношения к этой модели, это совсем другой вопрос, требующий анализа более высокого порядка, потому что решатель не может просто найти решение:нужно показать, что нет расширения этого решения, удовлетворяющего отрицательному ограничению.Ваш первоначальный пример подобен этому.

Итак, да, это фундаментальное ограничение в том смысле, что логика более высокого порядка принципиально менее поддающаяся изучению.Но является ли это ограничением для вас на практике, это другой вопрос.Какой анализ вам на самом деле нужен?

Одним из убедительных примеров использования формул более высокого порядка является синтез.Типичная проблема синтеза имеет вид «найди мне программную структуру P такую, что нет контрпримеров к спецификации S».Это требует анализа более высокого порядка и является той проблемой, для решения которой был разработан Alloy *.

Но, как правило, нет причин использовать Alloy * для стандартных задач проверки / моделирования.

...