Prolog program to enumerate all possible solution over a countable set

Question

I am writing a prolog program with can perform Peano arithmetics.

I have standard definitions for natural numbers.

nat(n).
nat(s(N)) :-
    nat(N).

Because I want to enumerate all possible relation of addition between natural numbers, I defined an auxiliary function (in order for defining total ordering over the set).

cmp_n(X, Y, lt) :-
    nat(Y),                % generate a stream : n s(n) s(s(n)) ...
    cmp_n_lt_helper(X, Y). % gives all XS smaller than Y

cmp_n_lt_helper(s(X), s(Y)) :-
    cmp_n_lt_helper(X, Y).
cmp_n_lt_helper(n, s(Y)) :-
    nat(Y).

Then, I defined addition

% need to use a wrapper because I want to generate (n, n, n) first
% if I don't use this warper, it would start from (n, s(n), s(n))
add_n(X, Y, R) :-
    nat(R),                  % same reason as above
    cmp_n(X, R, lt),
    add_n_helper(X, Y, R).

add_n_helper(s(X), Y, s(R)):-
    add_n_helper(X, Y, R).
add_n_helper(n, Y, Y).

If I enumerate all possible relations over this definition of addition, it worked fine. And when outputting a finite set of answers, it can halt.

?- add_n(X, Y, R).
X = Y, Y = R, R = n ;
X = R, R = s(n),
Y = n ;
X = n,
Y = R, R = s(n) ;
X = R, R = s(s(n)),
Y = n ;
X = Y, Y = s(n),
R = s(s(n)) ;
X = n,
Y = R, R = s(s(n)) .

?- add_n(X, Y, s(s(s(s(n))))).
X = s(s(s(s(n)))),
Y = n ;
X = s(s(s(n))),
Y = s(n) ;
X = Y, Y = s(s(n)) ;
X = s(n),
Y = s(s(s(n))) ;
X = n,
Y = s(s(s(s(n)))) ;
false.

These worked fine.

However, if I do the regular forward evaluation,

?- add_n(s(s(s(n))), s(s(n)), R).
R = s(s(s(s(s(n)))))

this program cannot halt.

I am wondering : is there a way to

for any finite answer, give a finite result.
for any infinite answer, fix a specific valid answer, give this specified answer in finite time

Your "generate a stream" line of nat(Y) is deliberately going off into infinity. In general, for a program to terminate sensibly, some common methods are: reduce towards e.g. 0 or an empty list, or use a cut after finding the one expected answer. — brebs, Dec 26 '21 at 14:30
Related: https://stackoverflow.com/questions/10139640/prolog-successor-notation-yields-incomplete-result-and-infinite-loop — brebs, Dec 26 '21 at 15:49
Yes I can do something like `add_n(n, Y, Y). add_n(s(X), Y, R) :- nat(R), cmp_n(X, R, le), add_n(X, s(Y), R).`. For forward calculation, this guarantee to terminate. However, when I run `?- add_n(X, Y, R).` It would only give me result from one branch i.e. `X = n, Y = R = n; X = n, Y = R = s(n) ...`. — liutaowen, Dec 26 '21 at 17:42
What I want to do is : let any combination of input (X, Y, R) give valid result. — liutaowen, Dec 26 '21 at 17:46
Not even Prolog can handle *infinity* in multiple inputs elegantly. One has to use e.g. nonvar(Input) to select a relevant answer path, and ultimately use e.g. must_be/2 (as in swi-prolog - https://www.swi-prolog.org/pldoc/man?predicate=must_be/2 ) to basically say "give me sensible input parameters" :-) — brebs, Dec 26 '21 at 18:14
Ohh, thank you! So, I need to specify the evaluation path for different input to handle this, right? — liutaowen, Dec 26 '21 at 20:25

score 0 · Accepted Answer · answered Dec 27 '21 at 14:58

As spot properly in the comments and by you as well, you've got a problem in a specific case, when X and Y are defined and R is not.

So let's just solve this case separately without the R generator in that case.

In my implementation (similar to yours)

nat(n).
nat(s(N)) :-
    nat(N).

eq_n(n, n) :- !.
eq_n(s(X), s(Y)) :-
    eq_n(X, Y), !.

leq_n(n, n).
leq_n(n, Y) :-
    nat(Y).
leq_n(s(X), s(Y)) :-
    leq_n(X, Y).

movel_n(X, n, X) :- !.
movel_n(X, s(Y), Z) :-
    movel_n(s(X), Y, Z), !.

add_n(X, Y, R) :-
    (   (   var(X)
        ;   var(Y)
        ),
        nat(R),
        leq_n(X, R),
        leq_n(Y, R)
    ;   \+ var(X),
        \+ var(Y), !
    ),
    movel_n(X, Y, Xn),
    eq_n(Xn, R).

The most important part for you is the first big or statement of add_n/3.

We're checking there with the var/1 if the variables are instantiated.

If not, we're creating the variables generator, otherwise, we're just going forward to calculations.

Thank you! This is very useful. However, I am wondering if there is any possible solution which doesn't use extra information like "var" or "novar"? — liutaowen, Dec 28 '21 at 20:23
AFAIK no. If you want to be able to produce solutions with uninstantiated variables, then you want to put some kind of solution generator (as you did) in the predicate. If you have a predicate with a generator then in some cases you'll end up with an endless loop (if the domain of variables is endless as it is here). — Armatorix, Dec 29 '21 at 11:26

Prolog program to enumerate all possible solution over a countable set

1 Answers1