普罗洛..。定义谓词，检查两个参数是否指向同一个原子

Question

我有一个prolog谓词，它接受两个参数(这里都标记为X，因为它们应该是相同的)，并比较它们是否计算出相同的原子。这就是目的所在。但是，当两个参数都是变量时，谓词意外地返回false。

我试图在Prolog中用句子逻辑/命题演算定义一个表达式为“隐含范式”的概念。这意味着所有连接词都被->和falsum替换。

作为一个基本情况，我想说的是，一个完全由原子组成的表达式本身已经处于正常状态。

以下是我试图表达的观点。我重复一个参数名，而不是对参数之间的同一性进行某种类型的检查。

% foo.P
implication_normal(X, X) :- atom(X).

这个不完整但仍然有用的定义旨在捕捉这样一个事实：implication_normal(x, x)是正确的，但implication_normal(x, y)是假的。

在某些方面，它似乎奏效了：

$ swipl -s foo.P

?- implication_normal(x, x).
true.

?- implication_normal(x, y).
false.

?- implication_normal(1, 1).
false.

它对变量做了错误的事情(它应该是枚举一对“绑定上下文”，其中X和Z恰好指向同一个原子)。

?- implication_normal(X, Z).
false.

如果给同一个变量两次，它也只返回false。

?- implication_normal(X, X).
false.

由于一些奇怪的原因，如果您给它一个变量和一个原子(如果使用一个整数就会失败)，那么这种行为是正确的。

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.

同样的，如果变量是第二个。

?- implication_normal(z, X).
X = z.

?- implication_normal(1, X).
false.

如何更改implication_normal的定义，以便在提供变量的所有情况下对其进行枚举？

Answer 1

标准的atom/1谓词是一个类型检查谓词.它不计数原子。它只是决定性地检查它的论点是否是一个原子。此外，您对implication_normal /2谓词的定义试图将统一它的两个参数，如果统一成功，则使用结果术语调用atom/1。这就是为什么像implication_normal(X, z)这样的调用成功的原因：X和z是统一的，atom(z)是真的。

请注意，一些Prolog系统提供了一个确实枚举原子的current_atom/1。在这些系统上，您可以写：

implication_normal(X, X) :- current_atom(X).

一些使用的示例调用：

?- implication_normal(X, Z).
X = Z, Z = '' ;
X = Z, Z = abort ;
X = Z, Z = '$aborted'
...

?- implication_normal(X, X).
X = '' ;
X = abort ;
X = '$aborted' ;
...

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.