How to implement the factorial sequence in successor arithmetics for all argument modes?

Question

The following Prolog program defines a predicate fact/2 for computing the factorial of an integer in successor arithmetics:

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).

It works with queries in this argument mode:

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

It also works with queries in this argument mode:

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

It also works with queries in this argument mode:

?- 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))))))
;  …

But it exhausts resources with queries in this argument mode:

?- 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>')

How to implement the factorial sequence in successor arithmetics for all argument modes?

Answer 1

The first question must be why? A failure-slice helps to understand the problem:

fact(0, s(0)) :- false.
fact(s(X), Y) :- fact(X, Z), false, prod(s(X), Z, Y).

This fragment alone terminates only if the first argument is given. If it is not, then there is no way to prevent non-termination, as Y is not restricted in any way in the visible part. So we have to change that part. A simple way is to observe that the second argument continually increases. In fact it grows quite fast, but for the sake of termination, one is enough:

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).

And, should I add, this can be even proved.

fact2(A,B)terminates_if b(A);b(B).
    % optimal. loops found: [fact2(s(_),s(_))]. NTI took    0ms,73i,73i

But, there is a caveat...

If only F is known, the program will now require temporally space proprotional to |F|! That is not an exclamation point but a factorial sign...