当我把它反过来说出来时，为什么Prolog找不到总和？

Posted 2021-04-18

假设我希望解决SWI-Prolog中列表的总和。最明显的解决方案是：

sum([],0).
sum([H|T],S) :- sum(T, SofT), S is SofT + H.

它完全按预期工作。

然而，出于好奇，我决定改写问题，说我们需要找到总和，使得尾部的总和是总和减去头部。应该是数学上相同的东西，尽管可能不那么自然。我把它写成了

sum2([],0).
sum2([H|T],S) :- sum2(T, S-H).

然后我用一个非常简单的测试用例执行我的查询并得到结果：

?- sum([1], S).
S = 1.

?- sum2([1], S).
false.

SWI-Prolog似乎无法回溯到sum2的解决方案，我想知道为什么会这样。我实际上有一种直觉，感觉事情可能会发生这种情况，但我仍然不确定这里到底发生了什么。我跑了一个示踪剂，但没有发现输出非常有启发性。我是Prolog的新手，所以我怀疑这个问题可能是愚蠢的，或暗示我的一些可怕的误解。

任何解释都将非常感谢，谢谢！

答案

根据this tutorial 鉴于两个术语T1和T2并且要统一：

• 如果T1和T2是常数（即原子或数字），那么如果它们是相同的成功。否则失败。
• 如果T1是变量，则将T1实例化为T2。
• 否则，如果T2是变量，则将T2实例化为T1。
• 否则，如果T1和T2是具有相同arity（参数个数）的复杂项，则找到T1的主要函子F1和T2的主函子F2。如果它们相同，则采用T1的有序参数集和T2的有序参数集。对于来自术语中相同位置的每对参数Am和Bm，Am必须与Bm统一。
• 否则失败。

所以当你跑步

?- sum2([1], S).

它已经运行了

sum2([],S-1)

已经统一的

sum2([],0)

并且它将S-1统一为0，其中0和1是常数，S是变量。 但是S-1不是常数也不是变量，所以它失败了。