Prolog program to enumerate all possible solution over a countable set

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

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

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.