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) 그렇지 처음부터 L을 평가 않습니다 예를 들면 볼 수 있듯이하지만 계산 :

다음 추적 모드에서 볼 수 있습니다 제약 조건을 검사합니다.

출처

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)에서 임의 길이의리스트를 생성 할 때 비 종단

답변

관련 문제