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.
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.