I like these versions of fac/2 a lot - not because they are so
beautiful, but because they tell us where Prolog is bad, and how
things could be improved.

Here is the first version in the SICStus manual:

     fac1(0, 1).
     fac1(N, X) :-
              N1 is N - 1,
              fac1(N1, Y),
              X is N * Y.

Let's have a look at what the SICStus manual says is the preferred
version of fac:

           fac_pref(N, X) :-
               (   N > 0 ->
                       N1 is N - 1,
                       fac_pref(N1, Y),
                       X is N * Y
               ;   N =:= 0 ->
                       X = 1
               ).

Note first the different semantics:

?- fac1(1-1,X).
ERROR: Out of local stack

?- fac1(2-1,X).

X = 1 ;
ERROR: Out of local stack

?- fac_pref(1-1,X).

X = 1

?- fac_pref(2-1,X).

X = 1

The fact that Prolog evaluates variables in arithmetic is very sneaky.
There is a good point NOT to do that.

In the "preferred" version, there is no good reason to have the
-> after the N =:= 0; a comma is fine. The -> suggests that there are
any choicepoints to be cut, but there aren't.

Now Jan's first version:

facjan1(N, X) :-
         N > 0, !,
         N1 is N - 1,
         facjan1(N1, Y),
         X is N * Y.
facjan1(0, 1) :- !.
facjan1(X, _) :-
         must_be(nonneg, X).

?- facjan1(1-1,X).
ERROR: Type error: `nonneg' expected, found `1-1'
    Exception: (11) throw(error(type_error(nonneg, 1-1), _G252)) ? creep
?- facjan1(2-1,X).

X = 1

Clearly not what one wants, and the origin is the same.
But Jan has a preferred version as well:

facjan_pref(N, I) :-
         must_be(nonneg, N),
         fac2(N, I).

fac2(0, 1) :- !.
fac2(N, X) :-
         N > 0, !,
         N1 is N - 1,
         fac2(N1, Y),
         X is N * Y.

?- facjan_pref(0,X).

X = 1
?- facjan_pref(1-1,X).
ERROR: Type error: `nonneg' expected, found `1-1'
    Exception: (11) throw(error(type_error(nonneg, 1-1), _G252)) ? creep

So, facjan_pref is explicit: the N must be a number (and an int and not negative).
In the other versions, there was no(t always) a need for that.

I guess the cut after the N > 0 test in the last clause remained there
because of cut&paste, so let's ignore it.

Now, the code for facjan_pref/fac2 specifies twice that the N must be
 > 0: once in the mustbe goal, and once in the second clause of fac2 -
how redeundant is that ...
But we cannot remove the last N > 0, because then we get

?- facjan_pref(0,7).
ERROR: Out of local stack

which is due to the first clause of fac2: it should have been

         fac2(0,Res) :- !, Res = 1.

Given that experts (Jan, Vitor) make subtle mistakes, and given the
pitfalls of floating point arithmetic (see what Joachim wrote), and
because of the pitfalls of unification (with 0 for instance) is quite
different from arithmetic equality testing (=:= 0) ...

wouldn't the following be a better way to write fac/2:

         :- type facbartpref(nonnegint:in, int:out). % (*)

         facbartpref(0,1).
         facbartpref(N,Res) :-
                 N \== 0,
                 M is N - 1,
                 facbartpref(M,Temp),
                 Res is N * Temp.

I have replaced the N > 0 by N \== 0. A decent compiler should be able
to avoid choicepoints, and if statically, it cannot prove that
facbartpref is called correctly, it can insert a minimal set of tests
to ensure this.

Why is the Prolog community still so scared of type/mode declarations,
when their advantage is so obvious.
(*) modulo choice of syntax and type system

Cheers