寻求(\=)/2的纯Prolog实现：能否仅用一阶Horn子句实现？

答案是不能——至少无法实现和内置(\=)/2完全等价的通用版本，核心原因在于纯Prolog（仅一阶Horn子句）的表达能力限制。

关键背景梳理 #

首先明确几个核心定义：

• 纯Prolog：仅由一阶Horn子句构成，只能进行正向推理，不包含失败否定（\+）、剪枝（!）这类非纯特性。
• 内置(\=)/2的语义：本质是否定的合一，即X \= Y成功当且仅当不存在任何替换能让X和Y合一（行为等价于\+ X = Y，但作为内置谓词效率更高）。

为什么纯Horn子句做不到？ #

Horn子句的核心局限是只能表达肯定性的事实和规则，无法直接断言“某个陈述不可能成立”：

1. 自由变量场景：当X和Y都是未绑定的自由变量时，内置X \= Y会失败（因为X = Y可以成功绑定两者）。但纯Prolog无法写出规则判断这种“不存在约束导致不等”的情况——你只能断言什么是相等的，无法断言什么是“不可能相等”的。
2. 通用递归判断：对于复合项（比如f(X) \= f(Y)），我们需要递归判断X \= Y，但这需要基于“X = Y不成立”的前提，而纯Horn子句无法将否定作为规则的触发条件。
3. 无法枚举所有项：你可以为特定基础项写规则（比如a \= b.、f(a) \= f(b).），但永远无法枚举所有可能的项组合，无法覆盖变量、嵌套复合项等通用场景。

总结 #

纯Prolog只能正向描述“什么是相等的”，但无法表达“什么是不可合一的”这种否定性的通用断言。要实现完整的(\=)/2语义，必须依赖SLDNF这类扩展了失败否定的推理机制，而这已经超出了纯一阶Horn子句的范畴。

内容的提问来源于stack exchange，提问作者user502187