代码之家 › 专栏 › 技术社区 › Greg Nisbet

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

prolog

Greg Nisbet · 技术社区 · 6 年前

我有一个prolog谓词,它接受两个参数(都有标签) X

我试图定义一个概念,在句子逻辑/命题演算中的表达式在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.

它对变量做了错误的事情(应该枚举“绑定上下文”对,其中 十 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 所以它枚举了所有提供变量的情况?

1 回复 | 直到 6 年前

Paulo Moura 6 年前

标准 atom/1 谓词是谓语。它不枚举原子。它只是确定地检查它的参数是否是一个原子。此外,你对 implication_normal /2 它的两个论点,如果统一成功,则调用以及由此产生的术语。这就是为什么 implication_normal(X, z) X 统一于 z atom(z) 这是真的。

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.