两个变体实现之间的差异

Question

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

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.

Answer 1

既没有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.

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

请注意,Xs上面不是变量名,而是(X)s.这s是一个双射,这是一个特殊的替代案例.

在这里,所有的例子都是指典型的用法bagof/3,setof/3其中变量总是不相交,但更微妙的情况是存在共同的变量.

在逻辑编程中,通常的定义是:

V是Tiff存在σ和θ 的变体

• 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)).

请注意,此替换替换了所有替换X并替换它们g(X).怎么会发生这种情况？事实上,Prolog的典型术语表示不能作为记忆中的图形发生.在Prolog中,节点在X某种程度上是内存中的真实地址,你完全不能进行这样的操作.但在逻辑上,事情完全是文本层面的.就像

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

除了一个还可以替换变量同时.想一想{ X ? Y, Y ? X}.它们必须立即更换,否则f(X,Y)会缩小为f(X,X)或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))已经失败.