Правило DLV небезопасно

Question

Я начинаю работать с DLV (Disjunctive Datalog), и у меня есть правило, сообщающее о ошибке «Правило небезопасно» при запуске кода. Правило следующее:

foo(R, 1) :- not foo(R, _) 

Я прочитал руководство и увидел, что «циклические зависимости запрещены». Я думаю, именно поэтому мне сообщают об ошибке, но я не уверен, как это утверждение так проблематично для DLV. Конечная цель - иметь некоторую инициализацию в случае, если предикат не был определен.

Точнее, если не существует «foo» с параметром R (и что-то еще), тогда определите его с параметрами R и 1. После того, как оно определено, правило не должно запускаться снова. Итак, это не настоящая рекурсия, на мой взгляд.

Любые комментарии о том, как решить эту проблему, приветствуются!

---

Я понял, что мне, вероятно, нужен еще один предикат, чтобы он соответствовал параметру R в теле правила. Что-то вроде этого:

foo(R, 1) :- not foo(R, _), bar(R) 

С, в противном случае не было бы никакого способа узнать, есть ли нет вхождений обув (R, _). Я не знаю, ясно ли я.

Во всяком случае, это не работает, либо :(

Answer 1

В частности, «Правило не является безопасной» ошибкой:. Прежде всего, это не имеет ничего общего с циклическими или ациклическими зависимостями То же сообщение об ошибке появляется на нециклическом программа:

foo2(R, 1) :- not foo(R,_), bar(R). 

проблема заключается в том, что программа на самом деле не безопасно (http://www.dlvsystem.com/html/DLV_User_Manual.html#SAFETY) Как уже упоминалось в разделе отрицательных правил (якорный # AEN375, я только разрешено использовать 2 ссылки в моей. ответ):

Variables, which occur in a negated literal, must also occur in a positive literal in the body.

Обратите внимание, что _ является анонимной переменной. То есть, программа

foo(R,1) :- not foo(R,_), bar(R). 

может быть эквивалентно записать в виде (и эквивалентен)

foo(R,1) :- not foo(R,X), bar(R). 

скрытых переменных (DLV руководство, якорь # AEN264 - в конце раздела) просто позволяют нам избегайте изобретать имена для переменных, которые будут встречаться только один раз в правиле (т. е. для переменных, которые выражают только «есть какое-то значение, я абсолютно не забочусь об этом), но они все равно являются переменными. И поскольку отрицание с не является« отрицанием », а не «истинное отрицание» (или «сильное отрицание», как его часто называют), ни одно из трех условий безопасности не удовлетворено правилом.

Очень грубая и высокоуровневая интуиция для безопасности заключается в том, что она гарантирует, что каждая переменная в программе может быть назначена какой-либо конечной области - так как теперь она имеет место с R, добавляя bar (R). Однако то же самое должно быть и для анонимной переменной _.

К актуальной задаче определения значений по умолчанию: Как указано lambda.xy.x, проблема здесь в семантике DLV для набора ответов (или стабильной модели): попытка сделать это в одном правиле не дает никакого решения: Чтобы получить безопасную программу, мы могли бы заменить вышеупомянутые проблемы, например. от

foo(1,2). bar(1). bar(2). 
tmp(R) :- foo(R,_). 
foo(R,1) :- not tmp(R), bar(R). 

Это не имеет устойчивой модели: Предположим, ответ есть, как задумано, {Foo (1,2), бар (1), бар (2), Foo (2,1)} Однако это не действительная модель, так как tmp (R): - foo (R, _) требует, чтобы она содержала tmp (2). Но тогда «не tmp (2)» перестает быть истинным, и поэтому наличие foo (2,1) в модели нарушает требуемую минимальность модели. (Это не совсем то, что происходит, более грубая интуиция. Более подробную информацию можно найти в любой статье по программированию на основе ответа, быстрый поиск в Google дал мне эту статью в качестве одного из первых результатов: http://www.kr.tuwien.ac.at/staff/tkren/pub/2009/rw2009-asp.pdf)

Чтобы решить проблему, поэтому необходимо «разбить цикл». Одним из возможных вариантов был бы:

foo(1,2). bar(1). bar(2). bar(3). 
tmp(R) :- foo(R,X), X!=1. 
foo(R,1) :- bar(R), not tmp(R). 

Т.е., явным образом о том, что мы хотим, чтобы добавить R в промежуточный атом, только если значение отличается от 1, имеющий Foo (2,1) в модели не противоречит TMP (2) не также является частью модели. Конечно, это больше не позволяет отличить, существует ли foo (R, 1) как значение по умолчанию или по вводу, но если это не требуется ...

Другой возможностью было бы не использовать foo для вычисления, но некоторые foo1. То есть имеющий

foo1(R,X) :- foo(R,X). 
tmp(R) :- foo(R,_). 
foo1(R,1) :- bar(R), not tmp(R). 

, а затем просто используйте foo1 вместо foo.