DLV 规则不安全

Question

我开始使用DLV（分离数据日志），并且在运行代码时，我有一条规则报告“规则不安全”错误。规则如下：

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

我已阅读手册并看到“不允许循环依赖”。我想这就是为什么我被报告错误的原因，但我不确定这个语句对 DLV 有什么问题。最终目标是在未定义谓词的情况下进行某种初始化。

更准确地说，如果没有出现带有参数 R（以及其他任何内容）的 'foo'，则使用参数 R 和 1 对其进行定义。一旦定义，则不应再次触发规则。所以，在我看来，这不是一个真正的递归。

欢迎任何有关如何解决此问题的 cmets！

---

我意识到我可能需要另一个谓词来匹配规则正文中的参数 R。像这样的：

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

既然如此，否则将无法知道是否没有出现 foo(R, _)。不知道我有没有说清楚。

无论如何，这也不起作用:(

Answer 1

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

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

问题是程序实际上并不安全（http://www.dlvsystem.com/html/DLV_User_Manual.html#SAFETY）。如关于否定规则的部分所述（锚#AEN375，我只能在我的答案中使用 2 个链接）：

出现在否定文字中的变量也必须出现在 正文中的正面文字。

注意 _ 是一个匿名变量。即程序

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

可以等价写成（并且等价于）

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

匿名变量（DLV 手册，锚点 #AEN264 - 在本节末尾）只是允许我们避免为只会在规则中出现一次的变量发明名称（即，对于仅表示“有一些价值，我绝对不关心它），但它们仍然是变量。由于非否定是“否定”而不是“真否定”（或通常称为“强否定”），因此三个安全条件都不是满足规则。

一个非常粗略和高级的安全直觉是，它保证程序中的每个变量都可以分配给某个有限域——就像现在通过添加 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 tmp(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) 不矛盾 不 em> 也是模型的一部分。当然，这不再允许区分 foo(R,1) 是作为默认值还是通过输入存在，但如果不需要...

另一种可能性是不使用 foo 进行计算，而是使用一些 foo1 。 IE。有

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

然后只使用 foo1 而不是 foo。