Prolog 程序枚举可数集上的所有可能解决方案

Question

我正在编写一个可以执行 Peano 算术的 prolog 程序。

我有自然数的标准定义。

nat(n).
nat(s(N)) :-
    nat(N).

因为我想枚举自然数之间所有可能的加法关系，所以我定义了一个辅助函数（为了定义集合上的总排序）。

cmp_n(X, Y, lt) :-
    nat(Y),                % generate a stream : n s(n) s(s(n)) ...
    cmp_n_lt_helper(X, Y). % gives all XS smaller than Y

cmp_n_lt_helper(s(X), s(Y)) :-
    cmp_n_lt_helper(X, Y).
cmp_n_lt_helper(n, s(Y)) :-
    nat(Y).

然后，我定义了加法

% need to use a wrapper because I want to generate (n, n, n) first
% if I don't use this warper, it would start from (n, s(n), s(n))
add_n(X, Y, R) :-
    nat(R),                  % same reason as above
    cmp_n(X, R, lt),
    add_n_helper(X, Y, R).

add_n_helper(s(X), Y, s(R)):-
    add_n_helper(X, Y, R).
add_n_helper(n, Y, Y).

如果我在这个加法的定义上列举所有可能的关系，它工作得很好。当输出有限的答案集时，它可以停止。

?- add_n(X, Y, R).
X = Y, Y = R, R = n ;
X = R, R = s(n),
Y = n ;
X = n,
Y = R, R = s(n) ;
X = R, R = s(s(n)),
Y = n ;
X = Y, Y = s(n),
R = s(s(n)) ;
X = n,
Y = R, R = s(s(n)) .

?- add_n(X, Y, s(s(s(s(n))))).
X = s(s(s(s(n)))),
Y = n ;
X = s(s(s(n))),
Y = s(n) ;
X = Y, Y = s(s(n)) ;
X = s(n),
Y = s(s(s(n))) ;
X = n,
Y = s(s(s(s(n)))) ;
false.

这些工作正常。

但是，如果我进行常规的前向评估，

?- add_n(s(s(s(n))), s(s(n)), R).
R = s(s(s(s(s(n))))) 

此程序无法停止。

我想知道：有没有办法

1. 对于任何有限的答案，给出一个有限的结果。
2. 对于任何无限答案，固定一个特定的有效答案，在有限时间内给出这个指定的答案

Answer 1

正如您在 cmets 中正确发现的那样，在特定情况下，当 X 和 Y 已定义而 R 未定义时，您会遇到问题。

所以让我们在这种情况下不使用 R 生成器单独解决这个情况。

在我的实现中（类似于你的）

nat(n).
nat(s(N)) :-
    nat(N).

eq_n(n, n) :- !.
eq_n(s(X), s(Y)) :-
    eq_n(X, Y), !.

leq_n(n, n).
leq_n(n, Y) :-
    nat(Y).
leq_n(s(X), s(Y)) :-
    leq_n(X, Y).

movel_n(X, n, X) :- !.
movel_n(X, s(Y), Z) :-
    movel_n(s(X), Y, Z), !.

add_n(X, Y, R) :-
    (   (   var(X)
        ;   var(Y)
        ),
        nat(R),
        leq_n(X, R),
        leq_n(Y, R)
    ;   \+ var(X),
        \+ var(Y), !
    ),
    movel_n(X, Y, Xn),
    eq_n(Xn, R).

对你来说最重要的部分是add_n/3 的第一个大or 声明。

如果变量已实例化，我们将使用var/1 进行检查。

如果没有，我们正在创建变量生成器， 否则，我们只是进行计算。