Datalog 的单面统一是不是足够？

Posted 2023-05-08

【中文标题】Datalog 的单面统一是不是足够？

【英文标题】：Is single sided unification sufficient for Datalog?Datalog 的单面统一是否足够？

【发布时间】：2021-05-25 02:34:36

【问题描述】：

Datalog 很容易用 Prolog 的一个子集来识别 不使用函数符号，而只使用常量和变量。 但是不使用否定的纯 Datalog 有进一步的约束（*）：

每一个事实都是有根据的。 规则头中的每个变量也出现在规则主体中。

我们能否得出结论，单面统一就足以 回答分层数据记录查询？或者有没有例子，可以证明 SWI-Prolog 8.3.19，单面有 (=>)/2

unfication，即纯 Datalog 但不以单面统一运行？

(*)你一直想知道的关于 Datalog 的知识 切里等。人。 - 1989https://www.researchgate.net/publication/3296132

【参考方案1】：

答案是否定的。对于最简单的 Datalog 事实和查询，直接转换为单面统一已经不起作用：

p(a).

?- p(X).
X = a

如果我们将 Prolog 事实 P 设为 P :- true，则通过 (=>)/2 将事实重写为 P => true。 SWI-Prolog 8.3.19 演示了这个东西不再起作用了：

p(a) => true.

?- p(X).
ERROR: No rule matches p(_2556)

甚至 Picat 也被这个问题所困扰，并且最初对事实进行了特殊处理。最近发布的 Picat v3 甚至重新引入了 Horn 子句。