Non-term when generating arbitrary length lists in CLP (FD)

Question

Why are the following exits with ERROR: Out of global stack after returning 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: Wrt @Joan answer, I'm trying to understand why it does not end, it is not necessary to find a solution that will end. I mean, if the problem is incoherence, then it should not evenly give an answer before labeling, right? Therefore, my question is more related to the mechanism for receiving answers (and does not end there) than the correction of the code.

Answer 1

The problem is that the predicate of length / 2 is persistent. You can find some posts to understand persistence in Stack Overflow, one good question from @mat: Steadfastness: Definition and its relation to logical cleanliness and completion . In simple words, persistence is a property that a predicate evaluates its parameters at the end.

In your example, you can specify the restrictions:

 L #>= 0, L #=< 3 

but in length(X, L). L will be graded at the end. So it happens that length(X, L) has infinite selection points (it will consider every list X), and for each list X it will evaluate L and, if L meets the restrictions, it will return you the answer and continue to study the next list which leads to an infinite loop.

In trace mode, you can see 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 to length([_G1110|_G1111], _G438) it does not evaluate L from the very beginning, but calculates it depending on the first argument and then checks the constraints.

Answer 2

This is simply because when the length is executed, it is still just an unrelated variable. This is not until:

• The scope of the restriction is reduced to a single value
• An unbound variable is combined with the actual value
• You are explicitly tagged with variables

So that the variable is bound to a single value.

You can correct your example by doing the following:

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

To see the first item, you can see that:

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

also works because the variable is limited to one value.