SWI-Prolog中考拉兹猜想不同实现失败原因咨询

我正在使用SWI-Prolog学习Prolog，参考某教程学习考拉兹猜想（Collatz Conjecture）。发现完全按照视频中的方式表达时，只要将#=替换为is（推测是SWI-Prolog与Scryer-Prolog的差异）就能正常运行，但稍微调整定义后就会出现错误或得出错误结论。以下是代码及问题分析：

use_module(library(clpfd)).

%% 可正常运行，collatz_next(A, 1) 返回 A=2
collatz_next(N0, N) :- 
    N0 is 2*N.
collatz_next(N0, N) :- 
   N0 is 2*_ + 1,
   N is 3*N0 + 1.

%% 无法运行，collatz_next(A, 1) 返回 false
%% collatz_next(N0, N) :- ((N0 mod 2) is 0),((N0 / 2) is N).
%% collatz_next(N0, N) :- ((N0 mod 2) is 1),((N0 * 3 + 1) is N).

%% 无法运行，collatz_next(A, 1) 返回 false
%% collatz_next(N0, N) :- ((N0 mod 2) is 0),(N0 is 2*N).
%% collatz_next(N0, N) :- ((N0 mod 2) is 1),((N0 * 3 + 1) is N).

%% 无法运行，报错"参数未充分实例化"
%% collatz_next(N0, N) :- 
%%    N0 / 2 is N.
%% collatz_next(N0, N) :- 
%%    N0 is 2*_ + 1,
%%    N is 3*N0 + 1.

核心问题：is谓词的单向性与实例化要求 #

Prolog中的is是算术求值谓词，有两个关键特性：

• 右侧的算术表达式必须完全实例化（所有变量都有具体数值），才能计算出确定结果。
• 它是单向的：要么将右侧计算结果赋值给左侧变量，要么比较左侧已实例化的值是否等于右侧结果，无法反过来从左侧推导右侧。

而视频中使用的#=是CLPFD（约束逻辑编程）库的双向约束谓词，支持部分实例化的变量，能进行双向推理——这是SWI-Prolog（用is）和Scryer-Prolog（用#=）的核心差异。

逐个分析失败的定义 #

1. 第二个定义（直接判断N0奇偶性）

当查询collatz_next(A, 1)时，N0是未实例化的变量A。子句中的(N0 mod 2) is 0要求N0必须是具体数值才能计算模2的结果，但此时N0未绑定，这个条件直接失败；第二个子句的(N0 mod 2) is 1同理无法求值，最终整个谓词返回false。

2. 第三个定义（先判断奇偶再关联N0与N）

问题和第二个定义完全一致：(N0 mod 2) is 0/1中的N0未实例化，mod操作无法执行，导致两个子句都失败，返回false。

3. 第四个定义（用除法推导N0）

第一个子句N0 / 2 is N中，当查询collatz_next(A,1)时，N是1，但N0是变量，右侧表达式N0/2包含未实例化的变量，无法计算确定值，触发参数未充分实例化错误。

为什么原版定义能运行？ #

原版第一个子句N0 is 2*N中，当查询collatz_next(A,1)时，N已经实例化为1，右侧2*1能直接计算出2，因此可以将N0绑定为2，子句成功匹配；第二个子句中N0 is 2*_ +1虽然用了匿名变量，但此时N0未绑定，这个子句会失败，但第一个子句已经成功，所以整体返回A=2。

如何写出支持双向推理的定义？ #

既然你已经导入了library(clpfd)，应该使用CLPFD的约束谓词替代is，这样无论变量是否实例化都能正常工作：

use_module(library(clpfd)).

collatz_next(N0, N) :-
    N0 #= 2*N.
collatz_next(N0, N) :-
    N0 mod 2 #= 1,
    N #= 3*N0 + 1.

这个版本既支持collatz_next(A,1)返回A=2，也支持collatz_next(3,N)返回N=10，甚至能处理更复杂的部分实例化查询。

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