% Reversible factorial relation
% fact(N, F) is true when F = N!
% Works when N is given, when F is given, or when both are variables.

% public entry
fact(N, F) :-
    (  nonvar(N) ->                % N is known: compute F directly
         integer(N), N >= 0,
         fact_from_n(N, F)
    ;  nonvar(F) ->                % F is known: search N by growing factorial
         integer(F), F >= 0,
         fact_from_f(F, N)
    ;  % both variables: enumerate N = 0,1,2,...
         nat(N),
         fact_from_n(N, F)
    ).

% compute factorial when N is known
fact_from_n(0, 1) :- !.
fact_from_n(N, F) :-
    N > 0,
    N1 is N - 1,
    fact_from_n(N1, F1),
    F is F1 * N.

% find N given F by iterative search
% handles F = 0 only if you want to treat 0 specially (0! = 1), so we require F >= 0
fact_from_f(F, N) :-
    % start search from 0 with accumulator 1
    fact_search(0, 1, F, N).

% fact_search(CurrentN, Acc, TargetF, ResultN)
fact_search(N, Acc, F, N) :-
    Acc =:= F, !.
fact_search(N, Acc, F, Res) :-
    Acc < F,
    N1 is N + 1,
    Acc1 is Acc * N1,
    fact_search(N1, Acc1, F, Res).
% If Acc > F the search fails (no integer N with N! = F).
% nat/1 enumerates natural numbers 0,1,2,...
nat(0).
nat(N) :- nat(M), N is M + 1.