factorial - Reversible numerical calculations in Prolog

Question

While reading SICP I came across logic programming chapter 4.4. Then I started looking into the Prolog programming language and tried to understand some simple assignments in Prolog. I found that Prolog seems to have troubles with numerical calculations.

Here is the computation of a factorial in standard Prolog:

f(0, 1).
f(A, B) :- A > 0, C is A-1, f(C, D), B is A*D.

The issues I find is that I need to introduce two auxiliary variables (C and D), a new syntax (is) and that the problem is non-reversible (i.e., f(5,X) works as expected, but f(X,120) does not).

Naively, I expect that at the very least C is A-1, f(C, D) above may be replaced by f(A-1,D), but even that does not work.

My question is: Why do I need to do this extra "stuff" in numerical calculations but not in other queries?

I do understand (and SICP is quite clear about it) that in general information on "what to do" is insufficient to answer the question of "how to do it". So the declarative knowledge in (at least some) math problems is insufficient to actually solve these problems. But that begs the next question: How does this extra "stuff" in Prolog help me to restrict the formulation to just those problems where "what to do" is sufficient to answer "how to do it"?

Answer 1

is/2 is very low-level and limited. As you correctly observe, it cannot be used in all directions and is therefore not a true relation.

For reversible arithmetic, use your Prolog system's constraint solvers.

For example, SWI-Prolog's CLP(FD) manual contains the following definition of n_factorial/2:

:- use_module(library(clpfd)).

n_factorial(0, 1).
n_factorial(N, F) :- N #> 0, N1 #= N - 1, F #= N * F1, n_factorial(N1, F1).

The following example queries show that it can be used in all directions:

?- n_factorial(47, F).
F = 258623241511168180642964355153611979969197632389120000000000 ;
false.

?- n_factorial(N, 1).
N = 0 ;
N = 1 ;
false.

?- n_factorial(N, 3).
false.

Of course, this definition still relies on unification, and you can therefore not plug in arbitrary integer expressions. A term like 2-2 (which is -(2,2) in prefix notation) does not unfiy with 0. But you can easily allow this if you rewrite this to:

:- use_module(library(clpfd)).

n_factorial(N, F) :- N #= 0, F #= 1.
n_factorial(N, F) :- N #> 0, N1 #= N - 1, F #= N * F1, n_factorial(N1, F1).

Example query and its result:

?- n_factorial(2-2, -4+5).
true .