1

我认为我对统一有一个根本的误解。这是我的两个子句：

test(func(X), X, 1) :- X == X.
test(func(X), Y, 0) :- X \== Y.

所以-如果我查询 test(func(X), Y, D)，我希望它只能用第二个子句证明，并且 D 将为 0。这是因为（我认为\我正在尝试）确保在第一个子句中，X 必须等于 X。所以我的查询不应该统一，因为 X 与 Y 不同。我认为 == 测试两个操作数是相同的变量。X 和 Y 显然不是。

但是输出：

| ?- test(func(X), Y, D).

D = 1
Y = X ? ;

D = 0

所以说如果Y = X，它与第一个子句统一。但是，Y不等于X。我在这里误解了什么？

4

2 回答 2

2

你的第一个答案，D = 1, Y = X符合你的第一个定义。我认为您期望查询?- test(func(X), Y, D).时第一个定义应该失败，因为X和Y是不同的变量，但第一个定义只有在两个变量相同时才应该成功。

但是，在您的子句的开头，您有两次出现相同的变量：（test(func(X), X, 1) :- X == X.正如@CapelliC 指出的那样，X == X这里是多余的。）当您查询时?- func(func(X), Y, D).，Prolog 尝试将此子句与您的第一条规则的开头统一起来。它func(X)与func(X)和Y与X和1结合1。一旦这种模式匹配统一成功，它就会测试规则的主体以查看是否满足条件。由于Y已与 统一X，两个变量将匹配严格相等条件---在模式匹配期间，您已统一Y与 相同的变量X。

请注意以下两个查询：

?- X == Y.
false.

?- Y = X, X == Y.
X = Y.

第二个类似于让您感到困惑的查询所发生的事情。如果您按照@CapelliC 的建议重写您的第一条规则，

test(func(X), Y, 1) :- X == Y.

然后它将按预期运行，因为在这种情况下，第二个参数中的自由变量将与func/1术语内的不同变量统一，然后两个变量将不满足严格相等（但如果两个变量与基本术语统一，它们将通过）。

于 2014-05-05T05:48:41.577 回答
1

X == X这是一种重言式（总是正确的），显然你的第一个子句可以等效地是

test(func(X), X, 1).

我认为你应该像第二个那样写

test(func(X), Y, 1) :- X == Y.
于 2014-05-05T05:24:24.103 回答