如何在所有参数模式的后继算术中实现阶乘序列？
How to implement the factorial sequence in successor arithmetics for all argument modes?
以下 Prolog 程序定义了一个谓词 fact/2 用于计算后继算术中整数的阶乘：
fact(0, s(0)).
fact(s(X), Y) :-
fact(X, Z),
prod(s(X), Z, Y).
prod(0, _, 0).
prod(s(U), V, W) :-
sum(V, X, W),
prod(V, U, X).
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
sum(X, Y, Z).
它适用于此参数模式下的查询：
?- fact(s(0), s(0)).
true
; false.
它也适用于此参数模式下的查询：
?- fact(s(0), Y).
Y = s(0)
; false.
它也适用于此参数模式下的查询：
?- fact(X, Y).
X = 0, Y = s(0)
; X = Y, Y = s(0)
; X = Y, Y = s(s(0))
; X = s(s(s(0))), Y = s(s(s(s(s(s(0))))))
; …
但是在这种参数模式下查询会耗尽资源:
?- fact(X, s(0)).
X = 0
; X = s(0)
;
Stack limit (0.2Gb) exceeded
Stack sizes: local: 4Kb, global: 0.2Gb, trail: 0Kb
Stack depth: 2,503,730, last-call: 100%, Choice points: 13
In:
[2,503,730] sum('<garbage_collected>', _1328, _1330)
[38] prod('<garbage_collected>', <compound s/1>, '<garbage_collected>')
[33] fact('<garbage_collected>', <compound s/1>)
[32] fact('<garbage_collected>', <compound s/1>)
[31] swish_trace:swish_call('<garbage_collected>')
如何在所有参数模式的后继算术中实现阶乘序列？
第一个问题一定是为什么？一个failure-slice有助于理解问题：
fact(0, s(0)) :- false.
fact(s(X), Y) :- fact(X, Z), false, prod(s(X), Z, Y).
仅当给出第一个参数时，该片段才会单独终止。如果不是，则无法防止不终止，因为 Y 在可见部分不受任何限制。所以我们必须改变那部分。一种简单的方法是观察第二个参数不断增加。其实长得挺快的，不过为了终止，一个就够了：
fact2(N, F) :-
fact2(N, F, F).
fact2(0, s(0), _).
fact2(s(X), Y, s(B)) :- fact2(X, Z, B), prod(s(X), Z, Y).
而且，我应该补充一下，这甚至可以是 proved。
fact2(A,B)terminates_if b(A);b(B).
% optimal. loops found: [fact2(s(_),s(_))]. NTI took 0ms,73i,73i
但是，有一个警告...
如果只知道 F，程序现在将暂时要求 space 与 |F| 成正比！那不是感叹号而是阶乘符号...
我认为当第二个参数是基础项时，你可以使用 cut 来避免回溯。
fact(0, s(0)).
fact(s(X), Y) :-
fact(X, Z),
prod(s(X), Z, W),
(ground(Y) ->
!,
Y = W
; Y = W).
prod(0, _, 0).
prod(s(U), V, W) :- sum(V, X, W), prod(V, U, X).
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :- sum(X, Y, Z).
示例：
?- fact(N, 0).
false.
?- fact(N, s(s(s(0)))).
false.
?- fact(X, s(0)).
X = 0
; X = s(0)
; false.
?- fact(s(s(s(0))), s(s(s(s(s(s(0))))))).
true
; false.
?- fact(s(s(s(0))), s(s(s(s(s(0)))))).
; false.
?- fact(s(s(s(0))), Y).
Y = s(s(s(s(s(s(0))))))
; false.
?- fact(X, Y).
X = 0, Y = s(0)
; X = Y, Y = s(0)
; X = Y, Y = s(s(0))
; …
?- fact(s(s(X)), s(s(Y))).
X = Y, Y = 0
; X = s(0), Y = s(s(s(s(0))))
; …
以下 Prolog 程序定义了一个谓词 fact/2 用于计算后继算术中整数的阶乘：
fact(0, s(0)).
fact(s(X), Y) :-
fact(X, Z),
prod(s(X), Z, Y).
prod(0, _, 0).
prod(s(U), V, W) :-
sum(V, X, W),
prod(V, U, X).
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :-
sum(X, Y, Z).
它适用于此参数模式下的查询：
?- fact(s(0), s(0)).
true
; false.
它也适用于此参数模式下的查询：
?- fact(s(0), Y).
Y = s(0)
; false.
它也适用于此参数模式下的查询：
?- fact(X, Y).
X = 0, Y = s(0)
; X = Y, Y = s(0)
; X = Y, Y = s(s(0))
; X = s(s(s(0))), Y = s(s(s(s(s(s(0))))))
; …
但是在这种参数模式下查询会耗尽资源:
?- fact(X, s(0)).
X = 0
; X = s(0)
;
Stack limit (0.2Gb) exceeded
Stack sizes: local: 4Kb, global: 0.2Gb, trail: 0Kb
Stack depth: 2,503,730, last-call: 100%, Choice points: 13
In:
[2,503,730] sum('<garbage_collected>', _1328, _1330)
[38] prod('<garbage_collected>', <compound s/1>, '<garbage_collected>')
[33] fact('<garbage_collected>', <compound s/1>)
[32] fact('<garbage_collected>', <compound s/1>)
[31] swish_trace:swish_call('<garbage_collected>')
如何在所有参数模式的后继算术中实现阶乘序列？
第一个问题一定是为什么？一个failure-slice有助于理解问题：
fact(0, s(0)) :- false. fact(s(X), Y) :- fact(X, Z), false,prod(s(X), Z, Y).
仅当给出第一个参数时，该片段才会单独终止。如果不是，则无法防止不终止，因为 Y 在可见部分不受任何限制。所以我们必须改变那部分。一种简单的方法是观察第二个参数不断增加。其实长得挺快的，不过为了终止，一个就够了：
fact2(N, F) :-
fact2(N, F, F).
fact2(0, s(0), _).
fact2(s(X), Y, s(B)) :- fact2(X, Z, B), prod(s(X), Z, Y).
而且，我应该补充一下，这甚至可以是 proved。
fact2(A,B)terminates_if b(A);b(B).
% optimal. loops found: [fact2(s(_),s(_))]. NTI took 0ms,73i,73i
但是，有一个警告...
如果只知道
F，程序现在将暂时要求 space 与 |F| 成正比！那不是感叹号而是阶乘符号...
我认为当第二个参数是基础项时，你可以使用 cut 来避免回溯。
fact(0, s(0)).
fact(s(X), Y) :-
fact(X, Z),
prod(s(X), Z, W),
(ground(Y) ->
!,
Y = W
; Y = W).
prod(0, _, 0).
prod(s(U), V, W) :- sum(V, X, W), prod(V, U, X).
sum(0, Y, Y).
sum(s(X), Y, s(Z)) :- sum(X, Y, Z).
示例：
?- fact(N, 0).
false.
?- fact(N, s(s(s(0)))).
false.
?- fact(X, s(0)).
X = 0
; X = s(0)
; false.
?- fact(s(s(s(0))), s(s(s(s(s(s(0))))))).
true
; false.
?- fact(s(s(s(0))), s(s(s(s(s(0)))))).
; false.
?- fact(s(s(s(0))), Y).
Y = s(s(s(s(s(s(0))))))
; false.
?- fact(X, Y).
X = 0, Y = s(0)
; X = Y, Y = s(0)
; X = Y, Y = s(s(0))
; …
?- fact(s(s(X)), s(s(Y))).
X = Y, Y = 0
; X = s(0), Y = s(s(s(s(0))))
; …