Prolog：为什么是 true == not(not(true)) -> false？

Question

显然true = not(not(true)) 必须为假，因为= 试图将原子true 与术语not(not(true)) 统一（不评估术语），这是错误的，因为术语不相同。

但是，我认为== 确实比较了评估的内容。因此，我认为true == not(not(true)) 应该评估为true == true，就像（对于算术运算符）4 =:= 2 + 2 将评估为4 =:= 4 并返回true。

...但这就是我在 SWI-Prolog 中得到的：

?- true == not(not(true)).
false.

我做错了什么？

Answer 1

(==)/2 不比较评估的内容。它不评估它的论点。只有当参数已经实例化为匹配项时，它才会成功。

在 prolog 中，not(not(true)) 是一个复合术语，它是带有单个参数 not(true) 的术语 not/1，它本身是一个术语 not/1 的一个参数，该参数由术语 true/0 组成，它没有论据。它没有价值。除非在某些情况下，它甚至不会被“执行”。在 Prolog 中，谓词 not/1 如果它的参数失败则成功，如果它的参数成功则它失败。这不是值或功能结果，而是一种行为。这是假设它出现在如下上下文中：

not(not(true)),
write('This will be written out because not(not(true)) succeeded'), nl.

Prolog 中的表达式true == not(not(true)) 是一个复合词，相当于：

'=='(true, not(not(true)))

在这种情况下，not(not(true)) 不会被评估。 Prolog 将首先使用(==)/2 等价运算符，如果其参数被实例化为相同的术语，则该运算符成功。 Prolog 中的术语true 和not(not(true)) 是否相同（或等效）？不，他们不是。一个是没有参数的简单术语 (true/0)。另一个是复合术语：具有一个参数的术语本身就是具有一个参数的术语。因此(==)/2 在这里失败了。

请注意，(=:=)/2 完全不同。它是一个比较算术表达式结果的运算符。参数必须是可计算的算术表达式，(=:=)/2 如果计算结果相同，则成功，否则失败。