Prolog가 자연수의 정의에 따라 수행하는 단계는 무엇입니까?

Question

나는 프롤로그에서 프로그램하는 방법을 배우고 난 자연의 숫자와 그 합 정의 다음 프로그램 발견

sum(succ(X), Y, succ(Z)) :- sum(X, Y, Z). 
sum(0, X, X). 
?- sum(succ(succ(0)), succ(succ(succ(0))), Answer). 
Answer = succ(succ(succ(succ(succ(0))))) 

(발견 here)

문제는 내가 함께 사투를 벌인거야 있다는 것입니다을 이 프로그램의 실행 흐름. 진실을 말하면 나는 그것이 무엇을하는지 모른다. 프롤로그는 어떻게 답변의 가치를 파악할 수 있습니까? Prolog가 답변의 가치를 찾기 위해 따라야 할 단계는 무엇입니까?

미리 감사드립니다.

Answer 1

기존의 술어를 알아 내거나 새로운 술어를 설계 할 때 Prolog가 작동하는 방식을 이해하는 데 도움이됩니다. 당신과 같은 쿼리를 만들 때 :

sum(succ(succ(0)), succ(succ(succ(0))), Answer). 

프롤로그 sum(_, _, _) (sum/3를) 일치하는 사실과 규칙 모양과 일치하는 첫 번째 하나를 선택합니다. 규칙은 다음과 같습니다.

(1) sum(succ(X), Y, succ(Z)) :- sum(X, Y, Z). 
(2) sum(0, X, X). 

쿼리를 보면 규칙 # 1의 패턴과 명확하게 일치합니다. Prolog에서 변수는 모든 종류의 용어로 인스턴스화 될 수 있고 동일한 이름의 변수는 단일화되어 (동일한 값으로 인스턴스화 됨) 기억하십시오. 프롤로그는 쿼리 규칙 # 1의 "머리"를 통합하면 다음과 같이 변수를 통일하여 그렇게 : Answer 할당 succ(Z)도 Z 불구하고이 구속되지 않은 값을 (이

X = succ(0) 
    Y = succ(succ(succ(0))) 
(A) Answer = succ(Z) 

공지하는 구체적인 가치). 이 sum/3에 대한 새 쿼리이기 때문에

sum(succ(0), succ(succ(succ(0))), Z) 
     |  |     | 
     X  Y     Z 

프롤로그 이제 다시 정상에서 시작됩니다 : 이제 우리는 쿼리 될 것입니다 쿼리합니다 규칙, sum(X, Y, Z)을 따릅니다. 그냥 처음처럼, 다음 통일화와 규칙 # 1 일치 : 나는 위의 Z'을 사용하고있는 sum(succ(0), succ(succ(succ(0))), Z)의 다른 변수 Z 구별하기 위해

X = 0 
    Y = succ(succ(succ(0))) 
(B) Z = succ(Z') 

, 그것이 사용 된 것과 다른 Z 때문에 머리는 sum(..., succ(Z))입니다. 이것은 C에서 int f(x) { return 2*x; }으로 선언 된 함수가 있고 어딘가에서 다른 로컬 변수 x으로 호출하면 그 이름이 x은 두 개의 다른 장소에서 사용되고 두 개의 다른 변수를 나타냅니다).

sum(0, succ(succ(succ(0))), Z') 
    | |     | 
    X Y     Z' 

이 재귀 쿼리는 succ(X) 일치하지 않는 첫 번째 인수, 0 때문에 규칙 # 1과 일치하지 않습니다

그럼 우리가되는, 다시 sum(X, Y, Z')을 다음 재귀 쿼리를 수행 할 수 있습니다.

0 = 0 
    X = succ(succ(succ(0))) 
(C) X = Z' 

이제 X = succ(succ(succ(0))) 그래서 Z' = succ(succ(succ(0))) : 그러나, 규칙 # 2 일치합니다. 이 룰에는 더 이상 질의가 없기 때문에 질의를받은 곳으로 마침내 성공합니다. 위의 (B)이 다시 돌아 :

Z = succ(Z') = succ(succ(succ(succ(0)))) 

및 (A)이 다시 돌아 :

Answer = succ(Z) = succ(succ(succ(succ(succ(0))))) 

을 그리고 거기 당신은 그것이있다. @CapelliC에서 언급 한 trace 기능을 사용하면 이러한 연속 단계가 Prolog 인터프리터에서 발생하는 것을 볼 수 있으며 변수의 인스턴스화를 따를 수 있습니다. 일치 대체에 따라, 프로그램의 규칙 '머리에 주어진 쿼리와 일치하고, 일치하는 규칙의 몸를 진행하여

Answer 2

과 같은 간단한 프로그램의 경우 trace/0 가야합니다. ,

21 ?- leash(-all),trace. 
true. 

[trace] 22 ?- sum(succ(succ(0)), succ(succ(succ(0))), Answer). 
    Call: (6) sum(succ(succ(0)), succ(succ(succ(0))), _G710) 
    Call: (7) sum(succ(0), succ(succ(succ(0))), _G789) 
    Call: (8) sum(0, succ(succ(succ(0))), _G791) 
    Exit: (8) sum(0, succ(succ(succ(0))), succ(succ(succ(0)))) 
    Exit: (7) sum(succ(0), succ(succ(succ(0))), succ(succ(succ(succ(0))))) 
    Exit: (6) sum(succ(succ(0)), succ(succ(succ(0))), succ(succ(succ(succ(succ(0)))))) 
Answer = succ(succ(succ(succ(succ(0))))). 

당신은 (통화 6 표시된 첫 번째 절 중 하나와 통일, 프로그램이 첫 번째 인수에 경계 재귀 검색을한다는 것을 볼 수 있습니다 leash/1 (초보자에 그 완전히 명확하지) 디버거 인터페이스를 조정할 수 있습니다 7) 또는 두 번째 호출 (8로 표시된 호출).

Answer 3

프롤로그의 "평가"진행. 규칙을 선택하면 그 변수는 균일 고유성, 이름이 변경됩니다 여기에서

 
(1) sum(succ(X), Y, succ(Z)) :- sum(X, Y, Z). 
(2) sum(0, X, X). 

    ?- sum(succ(succ(0)), succ(succ(succ(0))), Answer ). 
(1) -> sum(succ( X1 ), Y1     , succ(Z1)) :- sum(X1, Y1, Z1). 

     %% X1 = succ(0), Y1 = succ(succ(succ(0))), succ(Z1) = Answer. %% 

    -? sum(X1,    Y1,     Z1  ). 
    -? sum(succ(0 ),  Y1,     Z1  ). 
(1) -> sum(succ(X2),  Y2,     succ(Z2)) :- sum(X2, Y2, Z2). 

     %% X2 = 0, Y2 = Y1, succ(Z2) = Z1. %% 

    -? sum(X2,    Y2,     Z2  ). 
    -? sum(0,    Y2,     Z2  ). 
(2) -> sum(0,    X3,     X3  ).  %% DONE. %% 

     %% X3 = Y2, X3 = Z2. %% 

, Answer = succ(Z1) = succ(succ(Z2)) = succ(succ(X3)) = succ(succ(Y2)) = succ(succ (Y1)) = succ(succ(succ(succ(succ(0)))))합니다.