5

变体谓词的这两种实现之间是否存在任何逻辑差异？

variant1(X,Y) :-
 subsumes_term(X,Y),
 subsumes_term(Y,X).

variant2(X_,Y_) :-
  copy_term(X_,X),
  copy_term(Y_,Y),
  numbervars(X, 0, N),
  numbervars(Y, 0, N),
  X == Y.
4

1 回答 1

5

既不variant1/2也不variant2/2实施作为句法变体的测试。但出于不同的原因。

目标variant1(f(X,Y),f(Y,X))应该成功但失败了。对于某些两侧出现相同变量的情况，其variant1/2行为不符合预期。要解决此问题，请使用：

variant1a(X, Y) :-
   copy_term(Y, YC),
   subsumes_term(X, YC),
   subsumes_term(YC, X).

目标variant2(f('$VAR'(0),_),f(_,'$VAR'(0)))应该失败但成功。显然，variant2/2假设'$VAR'/1它的论点中没有发生。

ISO/IEC 13211-1:1995 定义变体如下：

7.1.6.1 术语的变体

如果前者的变量对后者的变量存在双射，则两个术语是变体s，使得后者的结果是将前者中的每个变量替换为.

X
Xs

笔记

1 例如，f(A, B, A)是 的变体f(X, Y, X)，
g(A, B)是 的变体g(_, _)，并且P+Q是 的变体
P+Q。

bagof/3
2 定义(8.10.2) 和setof/3(8.10.3)时需要变体的概念。

请注意，Xs上面不是变量名，而是 ( X) s。这里的双射也是如此s，它是替换的特例。

在这里，所有示例都指的是变量碰巧总是不相交的典型用法，但更微妙的情况是存在公共变量时bagof/3。setof/3

在逻辑编程中，通常的定义是：

V是T当且仅当存在 σ 和 θ 使得

  • Vσ 和T是相同的
  • Tθ 和V相同

换句话说，如果两者相互匹配，它们就是变体。然而，匹配的概念对于 Prolog 程序员来说是非常陌生的，即形式逻辑中使用的匹配概念。这是一个让许多 Prolog 程序员感到恐慌的案例：

考虑f(X)和f(g(X))。f(g(X))匹配还是不匹配f(X)？许多 Prolog 程序员现在会耸耸肩，对发生检查咕哝几句。但这与发生检查完全无关。他们匹配，是的，因为

f(X){ X↦ g(X)} 等同于f(g(X)).

请注意，此替换替换 allX并将它们替换为g(X). 这怎么可能发生？事实上，Prolog 的典型术语表示为内存中的图形是不可能发生的。在 Prolog 中，节点X是以某种方式在内存中的真实地址，您根本无法执行这样的操作。但在逻辑上，事情完全是在文本层面上。就像

sed 's/\<X\>/g(X)/g'

除了一个也可以同时替换变量。想想{ X ↦ Y, Y ↦ X}。它们必须立即更换，否则f(X,Y)会缩小为f(X,X)or f(Y,Y)。

因此，这个定义虽然形式上是完美的，但依赖于在 Prolog 系统中没有直接对应关系的概念。

当考虑不匹配的单边统一时，也会发生类似的问题，而是统一和匹配之间的常见情况。

根据 ISO/IEC 13211-1:1995 Cor.2:2012（草案）：

8.2.4 subsumes_term/2

这个内置谓词提供了对语法片面统一的测试。

8.2.4.1 说明

subsumes_term(General, Specific)为真，当且仅当存在替代θ使得

a) Generalθ 和Specificθ相同，并且
b) Specificθ和θSpecific 相同。

在程序上，subsumes_term(General, Specific)简单地相应地成功或失败。没有副作用或统一。

对于您的定义variant1/2，subsumes_term(f(X,Y),f(Y,X))已经失败。

于 2014-11-13T09:35:27.283 回答