在CLP（FD）中生成任意長度的列表時，未終止

爲什麼在返回預期答案後，ERROR: Out of global stack退出？在CLP（FD）中生成任意長度的列表時，未終止

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

更新：W.r.t. @瓊的回答，我試圖瞭解爲什麼它不終止，不一定找到解決方案，將終止。我的意思是，如果問題沒有束縛，那麼在標籤之前它不應該同樣產生任何答案，對吧？所以我的問題更多地涉及到生成答案的機制（而不是終止），而不是修復代碼。

來源

2016-12-15 Hugo Sereno Ferreira

問題是長度/ 2謂詞是堅定的。你可以在Stack Overflow中找到一些關於穩定性的帖子，@mat的一個好問題是：Steadfastness: Definition and its relation to logical purity and termination。簡而言之，堅定性是謂詞在最後評估其參數的屬性。

在你的榜樣，你可以給約束：

L #>= 0, L #=< 3

但length(X, L). L將在年底進行評估。那麼會發生什麼是length(X, L)有無限的選擇點（它將檢查每個列表X），並且對於每個列表X它將評估L，並且如果L滿足約束條件，那麼它將返回一個答案並繼續檢查下一個列表導致無限循環。

可以在跟蹤模式下看到以下內容：

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

正如你在第一次調用length([_G1110|_G1111], _G438)它不會從一開始就評估拭目以待例如但計算它取決於第一個參數，然後檢查約束。

來源

2016-12-15 19:54:17 coder

這只是因爲長度運行時，它仍然只是一個未綁定的變量。它不是直到：

約束的域減少爲單個值
未綁定變量是統一的實際值
您明確標註變量

該變量將被綁定到一個單一的值。

您可以通過執行解決您的例子：

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

要查看你可以看到，第一點：

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

也適用，因爲變量被限制爲單個值。

來源

2016-12-15 16:44:37 Joan

在CLP（FD）中生成任意長度的列表時，未終止

回答

相關問題