如何使用succ通過遞歸查詢運行prolog？

有人可以向我解釋爲什麼這個序言查詢的工作方式。該定義是：如何使用succ通過遞歸查詢運行prolog？

add(0,Y,Y). 
add(succ(X),Y,succ(Z)):- add(X,Y,Z).

鑑於此：

?- add(succ(succ(succ(0))), succ(succ(0)), R).

繼承人的查詢跟蹤：

Call: (6) add(succ(succ(succ(0))), succ(succ(0)), R) 

Call: (7) add(succ(succ(0)), succ(succ(0)), _G648) 

Call: (8) add(succ(0), succ(succ(0)), _G650) 

Call: (9) add(0, succ(succ(0)), _G652) 

Exit: (9) add(0, succ(succ(0)), succ(succ(0))) 

Exit: (8) add(succ(0), succ(succ(0)), succ(succ(succ(0)))) 

Exit: (7) add(succ(succ(0)), succ(succ(0)), 
               succ(succ(succ(succ(0))))) 

Exit: (6) add(succ(succ(succ(0))), succ(succ(0)), 
               succ(succ(succ(succ(succ(0))))))

是困惑我最瞭解該教程是事實的一部分，在第一個參數，succ被剝離，並且它遞歸。雖然遞歸雖然，R獲得succ ...如何？！另外，零在哪裏從第一個出口（9）出發？我對prolog很陌生，我正在努力理解作業的語言。任何幫助非常感謝。先謝謝了。

注：有興趣的人，鏈接，本教程是http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse9

來源

2012-04-25 Andy

通常，'succ/1'寫成's/1'。請看標籤[tag：successor-arithmetics]的答案。 – false 2012-04-25 07:24:35

「哪裏零來自在第一個出口（9）？」

呼叫add(0, succ(succ(0)), _G652)是統一的，說的是，如果add第一個參數是零，那麼第二個和第三個是相同的第一條。在這個特定的情景變量_G652變成succ(succ(0))。

「雖然遞歸，但R獲得了成功......如何？！」

這是應用第二個子句的結果。本條款（粗略地）聲明，您首先從第一個參數中剝離succ，然後遞歸地調用add，最後，向從此遞歸調用返回的第三個參數添加另一個「層」succ。

謂詞add不過在皮亞諾算術直接實現加：http://en.wikipedia.org/wiki/Peano_axioms#Addition

來源

2012-04-25 06:14:16

我明白你在說什麼了，我對此多瞭解一點。我不理解的是，規則的頭也在做一些事情，我只是假設它沒有做任何事情，直到屍體被證明。 – Andy 2012-04-25 19:19:27

你看，call和exit是verbs，行動的解釋採取試圖解決您提出的查詢。然後跟蹤將顯示已完成的實際工作的詳細信息，並讓您以歷史視角查看它。

當Prolog的必然選擇規則（一call），它使用你給它name（所謂functor），並試圖以unify在規則的頭上，每種說法。然後我們通常會說Prolog也考慮了arity，即參數的數量，以供選擇。

Unification試圖使'等於'兩個詞，而值得注意的結果是所謂的bindings變量。您已經知道變量是從Uppercase開始的那些名稱。這些名稱標識規則中未指定的值，即參數爲placeholders。爲了避免混淆，當Prolog顯示跟蹤時，變量被重命名，以便我們可以識別它們，因爲相關的細節是identities或證據期間建立的綁定。

然後你會看到跟蹤中的這樣的_G648符號。他們停留在尚未被實例化的被叫目標的論點，即R和Z。 R是唯一的（只發生在頂級調用中），所以這個Prolog很好地保持用戶友好的名稱，但是Z來自程序，可能會多次出現，然後重新命名。

爲了回答這個查詢

?- add(succ(succ(succ(0))), succ(succ(0)), R).

Prolog的第一次嘗試，以匹配

add(0,Y,Y).

和失敗，因爲SUCC（SUCC（SUCC（0））不能進行等於0 然後企圖

add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

因此必須解決這些綁定（向左調用者的條款）：

succ(succ(succ(0))) = succ(X) 
succ(succ(0)) = Y 
R = Z

你可以看到爲什麼X變得succ(succ(0))，我們有一個新的目標來證明，即規則主體add(X,Y,Z)與剛成立的綁定：

加（SUCC（SUCC（0）），SUCC （SUCC（0）），_ G648）

等等......直到X變得0和目標相匹配

add(0,Y,Y).

然後Y變成succ（succ（0）），值得注意的是在調用規則中給出了Z的值。

HTH

來源

2012-04-25 06:37:18 CapelliC

如何使用succ通過遞歸查詢運行prolog？

回答

相關問題