Non-termination when generating lists of arbitrary length in CLP(FD) [duplicate]

Question

Why does the following exits with a ERROR: Out of global stack after return the expected answers?

?- L #>= 0, L #=< 3, length(X, L).

L = 0,
X = [] ;
L = 1,
X = [_G1784] ;
L = 2,
X = [_G1784, _G1787] ;
L = 3,
X = [_G1784, _G1787, _G1790] ;
ERROR: Out of global stack

---

Update: W.r.t. @Joan's answer, I'm trying to understand why it doesn't terminate, not necessarily finding a solution that would terminate. I mean, if the problem is unboundness then it shouldn't equally produce any answer until the labelling, right? So my question is more related to the mechanism of producing answers (and not terminating), than fixing the code.

Answer 1

The problem is that the length/2 predicate is steadfast. You can find some posts to understand about steadfastness in Stack Overflow, one good question by @mat is: Steadfastness: Definition and its relation to logical purity and termination. In simple words steadfastness is the property that a predicate evaluates it's parameters at the end.

In your example you may give the constraints:

L #>= 0, L #=< 3

but in length(X, L). L will be evaluated at the end. So what happens is that length(X, L) has infinite choice points (it will examine every list X) and for every list X it will evaluate L and, if L meets the constraints then it will return you an answer and will go on to examine the next list which leads to infinite loop.

You can see in trace mode the following:

  Call: (8) length(_G427, _G438) ? creep
   Exit: (8) length([], 0) ? creep
   Call: (8) integer(0) ? creep
   Exit: (8) integer(0) ? creep
   Call: (8) 0>=0 ? creep
   Exit: (8) 0>=0 ? creep
   Call: (8) integer(0) ? creep
   Exit: (8) integer(0) ? creep
   Call: (8) 3>=0 ? creep
   Exit: (8) 3>=0 ? creep
X = [],
L = 0 ;
   Redo: (8) length(_G427, _G438) ? creep
   Exit: (8) length([_G1110], 1) ? creep
   Call: (8) integer(1) ? creep
   Exit: (8) integer(1) ? creep
   Call: (8) 1>=0 ? creep
   Exit: (8) 1>=0 ? creep
   Call: (8) integer(1) ? creep
   Exit: (8) integer(1) ? creep
   Call: (8) 3>=1 ? creep
   Exit: (8) 3>=1 ? creep
X = [_G1110],
L = 1 ;
   Redo: (8) length([_G1110|_G1111], _G438) ? creep
   Exit: (8) length([_G1110, _G1116], 2) ? creep
   Call: (8) integer(2) ? creep
   Exit: (8) integer(2) ? creep
   Call: (8) 2>=0 ? creep
   Exit: (8) 2>=0 ? creep
   Call: (8) integer(2) ? creep
   Exit: (8) integer(2) ? creep
   Call: (8) 3>=2 ? creep
   Exit: (8) 3>=2 ? creep
X = [_G1110, _G1116],
L = 2 ;
   Redo: (8) length([_G1110, _G1116|_G1117], _G438) ? creep
   Exit: (8) length([_G1110, _G1116, _G1122], 3) ? creep
   Call: (8) integer(3) ? creep
   Exit: (8) integer(3) ? creep
   Call: (8) 3>=0 ? creep
   Exit: (8) 3>=0 ? creep
   Call: (8) integer(3) ? creep
   Exit: (8) integer(3) ? creep
   Call: (8) 3>=3 ? creep
   Exit: (8) 3>=3 ? creep
X = [_G1110, _G1116, _G1122],
L = 3 ;
 Redo: (8) length([_G1110, _G1116, _G1122|_G1123], _G438) ? creep
   Exit: (8) length([_G1110, _G1116, _G1122, _G1128], 4) ? creep
   Call: (8) integer(4) ? creep
   Exit: (8) integer(4) ? creep
   Call: (8) 4>=0 ? creep
   Exit: (8) 4>=0 ? creep
   Call: (8) integer(4) ? creep
   Exit: (8) integer(4) ? creep
   Call: (8) 3>=4 ? creep
   Fail: (8) 3>=4 ? creep

As you can see for example in the first call length([_G1110|_G1111], _G438) it doesn't evaluates L from the beginning but it calculates it depending the first argument and then checks the constraints.

Answer 2

That's just because when length is run, it's still just an unbound variable. It's not until:

• The domain of the constraint is reduced to a single value
• The unbound variable is unified with an actual value
• You explicitly label the variables

That the variable will be bound to a single value.

You can fix your example by doing:

?- L #>= 0, L #=< 3, label([L]), length(X, L).

To see the first point you can see that:

?- L #>= 1, L #=< 1, length(X, L).

also works because the variable is constrained to a single value.