Prolog ...定义检查两个参数是否/指向同一个原子的谓词答案

【问题标题】：Prolog ... define predicate that checks if both arguments are/point to the same atomProlog ...定义检查两个参数是否/指向同一个原子的谓词
【发布时间】：2018-09-25 00:27:36
【问题描述】：

我有一个序言谓词，它接受两个参数（这里都标记为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 的定义，以便在提供变量的所有情况下进行枚举？

【问题讨论】：

标签： prolog

【解决方案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).

使用 SWI-Prolog 的一些示例调用：

?- 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.

【讨论】：

所以，我确实尝试了imp_norm(X, Z) :- p_variable(x), p_variable(Z), X = Z.，这似乎奏效了。使用imp_norm(X, X) :- current_atom(X) 和imp_norm(X, Z) :- current_atom(X), current_atom(Z), X = Z 之间有什么区别吗？
第一个会比第二个快。