DLV规则不安全

Question

我开始使用DLV (析取数据)，并且在运行代码时，我有一个规则，即报告一个“规则是不安全的”错误。规则如下：

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

我已经阅读了手册，并看到“循环依赖是不允许的”。我想这就是为什么我被报告了这个错误，但我不知道这个声明为什么会对DLV造成如此大的问题。最终目标是在没有定义谓词的情况下进行某种类型的初始化。

更准确地说，如果参数R(和其他任何东西)都没有出现“foo”，那么使用参数R和1来定义它。一旦定义好了，规则就不应该再触发了。所以，在我看来，这不是一个真正的递归。

欢迎任何关于如何解决这个问题的意见！

我已经意识到，我可能需要另一个谓词来匹配规则主体中的参数R。就像这样：

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

因为，否则就无法知道foo(R，_)是否出现。我不知道我是否说得很清楚。

无论如何，这也不起作用：

Answer 1

对于特定的“规则不安全”错误:首先，这与循环或非循环依赖无关。对于非循环程序也会显示相同的错误消息：

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

问题是程序实际上是不安全的(Manual.html#SAFETY)。正如否定规则一节(锚# am 375，我只能在我的答案中使用两个链接)：

变量出现在否定的文本中，也必须出现在正文中的正文本中。

注意，_是一个匿名变量。也就是说，程序

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

可以等效地写成(和等效于)

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

匿名变量(DLV手册，锚# as 264-在本节末尾)只允许我们避免为只在规则中出现一次的变量(即只表示“有一些值，我绝对不关心它)的变量创建名称”，但是它们仍然是变量。由于否定不等于“否定”，而不是“真正的否定”(也常被称为“强否定”)，所以这三种安全条件都不能满足。

对于安全的一个非常粗糙和高层次的直觉是，它保证程序中的每个变量都可以被分配到某个有限域--就像现在通过添加bar(R)来处理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)，bar(1)，bar(2)，foo(2,1)}但是，这不是一个有效的模型，因为tmp(R) :- foo(R，_)将要求它包含tmp(2)。但是，"not (2)“不再是真，因此在模型中使用foo(2,1)违反了模型所需的最小性。(这不是正在发生的事情，更多的是一种粗略的直觉。更多的技术细节可以在任何一篇关于答案集编程的文章中找到，谷歌快速搜索给我的第一篇文章是：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).

也就是说，通过明确声明只有当值与1不同时，我们才想将R添加到中间原子中，在模型中有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。