原有的后继算术阶乘程序在正向查询（已知X求Y）或双向查询（X和Y都未绑定）时能正常工作，但在**已知Y求X**的反向查询（比如?- fact(X, s(0)).）中会耗尽堆栈资源。

原因在于：当Y固定为s(0)时，Prolog在找到X=0和X=s(0)后，会继续尝试生成更大的X值（s(s(0))、s(s(s(0)))...），并不断递归计算它们的阶乘——而这些阶乘显然会大于s(0)，但程序没有任何机制停止这种无限尝试，最终导致栈溢出。

要让阶乘谓词在所有参数模式下都能正确终止并返回结果，我们需要给程序添加终止条件，或者调整谓词的执行顺序，让生成过程受到目标值的约束。下面提供两种可行的方案：

方案1：生成-测试模式（带终止条件） #

我们可以先按顺序生成自然数，计算每个数的阶乘，然后与目标Y匹配。关键是当计算出的阶乘超过目标Y时，停止生成更大的数（因为后继算术中，更大的数的阶乘只会更大）。

首先定义一个比较后继算术数大小的leq/2谓词（判断小于等于）：

leq(0, _).
leq(s(X), s(Y)) :- leq(X, Y).

然后修改fact/2为生成-测试的形式，结合自然数生成、阶乘计算和终止约束：

% 生成自然数序列：0, s(0), s(s(0)), ...
nat(0).
nat(s(X)) :- nat(X).

% 带终止条件的通用阶乘谓词
fact(X, Y) :-
    nat(X),
    fact_calc(X, Y),
    % 当Y已绑定时，若当前阶乘超过Y则停止后续生成
    (var(Y) -> true ; leq(Y, fact_calc(X, _)) -> ! ; true).

% 原有的阶乘计算核心逻辑
fact_calc(0, s(0)).
fact_calc(s(X), Y) :- fact_calc(X, Z), prod(s(X), Z, Y).

% 修正后的乘积谓词（确保递归方向正确）
prod(0, _, 0).
prod(s(U), V, W) :- sum(V, X, W), prod(U, V, X).

% 原有的求和谓词
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :- sum(X, Y, Z).

这个版本中，当查询?- fact(X, s(0)).时，程序会生成X=0（阶乘匹配）、X=s(0)（阶乘匹配），然后生成X=s(s(0))，计算其阶乘为s(s(0))——此时s(s(0))大于s(0)，触发截断操作!，停止后续生成，避免无限递归。

方案2：改进基础谓词（适配所有参数模式） #

另一种方法是让sum/3和prod/3在所有参数模式下都能终止，通过添加显式的参数绑定判断，选择不同的执行路径：

% 自然数生成
nat(0).
nat(s(X)) :- nat(X).

% 改进的sum/3：适配所有参数模式
sum(A, B, C) :-
    (var(A), var(B), var(C)) -> nat(A), sum(A, B, C) ;
    (var(A)) -> sum_aux(B, C, A) ;
    (var(B)) -> sum_aux(A, C, B) ;
    sum_verify(A, B, C).

sum_aux(0, C, C).
sum_aux(s(X), s(C), A) :- sum_aux(X, C, A).

sum_verify(0, B, B).
sum_verify(s(X), B, s(C)) :- sum_verify(X, B, C).

% 改进的prod/3：适配所有参数模式
prod(A, B, C) :-
    (var(A), var(B), var(C)) -> nat(A), prod(A, B, C) ;
    (A = 0) -> C = 0 ;
    (var(A)) -> prod_aux(B, C, A) ;
    (var(B)) -> prod_aux(A, C, B) ;
    prod_verify(A, B, C).

prod_aux(0, 0, _).
prod_aux(s(U), W, s(V)) :- sum(V, X, W), prod_aux(U, X, V).

prod_verify(0, _, 0).
prod_verify(s(U), V, W) :- sum(V, X, W), prod_verify(U, V, X).

% 通用阶乘谓词
fact(0, s(0)).
fact(s(X), Y) :- fact(X, Z), prod(s(X), Z, Y).

这个版本的sum/3和prod/3会根据参数的绑定情况选择执行逻辑：当目标值绑定后，会通过反向求解的方式计算输入，而不会无限生成更大的数。查询?- fact(X, s(0)).时，程序会正确返回X=0和X=s(0)，然后停止。

现在测试所有参数模式的查询效果：

1. 正向验证：

?- fact(s(0), s(0)).
true ; false.

2. 求阶乘结果：

?- fact(s(0), Y).
Y = s(0) ; false.

3. 双向生成所有阶乘对：

?- fact(X, Y).
X = 0, Y = s(0) ;
X = s(0), Y = s(0) ;
X = s(s(0)), Y = s(s(0)) ;
X = s(s(s(0))), Y = s(s(s(s(s(s(0)))))) ;
... % 可按Ctrl+C停止

4. 反向查询（已知结果求输入）：

?- fact(X, s(0)).
X = 0 ;
X = s(0) ;
false. % 无栈溢出，正确终止

内容的提问来源于stack exchange，提问作者Géry Ogam