CLPFD and infinite countable domains

The reason for this is that CLP(FD) preserves the following important property:

If a predicate p(Vs) terminates universally, then ?- p(Vs), label(Vs). also terminates universally.

A goal G terminates universally iff ?- G, false. terminates.

Why is this so important? Because a CLP(FD) program typically consists of two parts:

1. posting all constraints
2. the search for solutions.

It is often easy to show, by simple inspection, that the modeling part (1) terminates universally. But (2) is the tough part that usually takes most of the computation time, and often we do not know a priori whether there even is a single solution. The search part may run for days, months or years without yielding results.

Many Prolog beginners describe a search task, run it, and after a few seconds complain that Prolog is slow. In reality, as it turns out, they often accidentally write programs that do not terminate, and can never find a solution.

For such reasons, it is encouraging that if you can only show (as you typically can, and also rather easily) that part (1) terminates, then your whole program—part (1) and part (2)—also terminates.

You are completely right that any countably infinite search space can be systematically covered to any finite extent in one of the ways you are describing. However, doing so would break this fundamental invariant. You must be able to count on the following property for the above reasoning to apply:

label/1, labeling/2 and indomain/1 always terminate.

In SWI-Prolog and YAP, this is ensured by design. In other systems it holds to varying degrees.

There is no reason to not allow infinite domains enumeration in CLP(FD). Since as user:mat has correctly observed the constraints itself terminate, an infinite enumeration might find a solution if a solution exists.

So basically we have:

The constraints terminate universally, i.e. (#=)/2, (#=<)/2, etc.. give true or false when completely instantiated, and don't diverge.

And we then observe:

The labeling of constraints terminates existentially, i.e. it finds a solution to a problem after some time if we can also enumerate multiple infinite domains in a fair way.

So the main problem is to enumerate multiple infinite domains in a fair way, since when we don't enumerate in a fair way, we might go astray in a subset of the domain and not find a solution even if there exists one. The following approaches to enumerate multiple infinite domains come to mind:

1) Unpair Function
Use a function unpair: N -> NxN, and enumerate the argument of this function only. This is an old Mathematica technique described here: An Elegant Pairing Function . Drawback you need to compute the square root each time.

2) Fair Conjunction
Use a fair conjunction to combine infinite enumerators. This is a technique applied in functional programming, see for example here: Backtracking, Interleaving, and Terminating Monad Transformers . Drawback the connective doesn't work in constant memory space, you spawn more and more instances of the right hand side enumerator.

3) Extra Variable
Use an extra variable H and an extra constraint for example H=abs(X1)+..+abs(Xn) for cantor pairing. You can then enumerate this variable and let the constraint solver do the rest of the work. Advantage for certain values you might have early pruning.

In Jekejeke Minlog we have recently opted for variant 3. Here is an example run to enumerate Pythagorean triples:

?- use_module(library(finite/clpfd)).

?- [X,Y,Z] ins 1..sup, X*X+Y*Y #= Z*Z, label([X,Y,Z]).
X = 3,
Y = 4,
Z = 5 ;
X = 4,
Y = 3,
Z = 5 ;
X = 6,
Y = 8,
Z = 10 ;
X = 8,
Y = 6,
Z = 10 

In general when using infinite labeling one will attempt to solve a Diophantine Equation, which do not have always a solution and this is even not decidable, which we know after Hilbert's Tenth problem came up. So a guarantee of universal termination is even not possible.

On the other hand if there is a solution, you might find it after some time, provided the solution is not too big and will exceed the computer limitations in memory space and computation time. But this shouldn't crash your computer, a decent Prolog system implementation should gracefully return to the top-level. You can also interrupt the interpreter or stop demanding further solutions.

Bye