Prolog谓词顺序变更触发nat_cset/2无限循环是否为合理行为咨询

问题定性 #

这个表现是当前nat_cset/2实现下的合理行为，但属于设计缺陷。它不符合纯单调谓词的实例化无关终止性要求，也就是你提到的丧失了纯谓词属性：谓词的终止性和结果正确性依赖调用时的参数实例化状态以及目标顺序，不符合声明式编程的预期。

根因说明 #

当前实现采用默认的SLD深度优先搜索逻辑，当N未实例化时调用nat_cset/2：

1. 第一个子句匹配N=0返回第一组解
2. 回溯时进入第二个子句，N #> 0会将N约束到1到无穷大的区间，递归调用时新的N_1仍然处于未实例化的约束状态
3. 搜索过程会无限枚举更大的N值，永远不会主动停止，所以nat_cset(N,Cs), N = 6, false.会进入死循环
   而先绑定N=6再调用时，N是确定值，递归到N=0就会终止，不会触发无限枚举逻辑。

优化方案 #

可以通过延迟执行的思路修改实现，保证谓词只有在参数足够实例化时才执行，避免未绑定参数时的无限递归，修改后代码如下：

% 加入延迟执行守卫，N或Cs有一个被实例化才执行实际逻辑
nat_cset(N, Cs) :-
    when((ground(N); ground(Cs)), nat_cset_(N, [], Cs)).

nat_cset_(0, Acc, Acc).
nat_cset_(N, Acc, Cs) :- 
    N #> 0, 
    N_1 #= N - 1,  
    nat_cset_(N_1, [N|Acc], Cs).

如果需要更精细的分支控制，也可以显式判断参数实例化状态：

nat_cset(N, Cs) :-
    (   % N已绑定，直接执行
        nonvar(N) ->
        nat_cset_(N, [], Cs)
    ;   % Cs已绑定为列表，先通过长度得到N再执行
        is_list(Cs) ->
        length(Cs, N),
        nat_cset_(N, [], Cs)
    ;   % 都未绑定，冻结调用等待N实例化
        freeze(N, nat_cset(N, Cs))
    ).

优化后验证 #

修改后两种调用顺序都可以正常终止：

?- nat_cset(N,Cs), N = 6, false.
false.

?- N = 6, nat_cset(N,Cs), false.
false.

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