Prolog後繼符號產生不完全結果和無限循環

Question

我開始學習Prolog並首先了解後繼符號。

這就是我在Prolog中找到關於編寫Peano公理的地方。在PDF的

見第12頁：

sum(0, M, M). 
sum(s(N), M, s(K)) :- 
    sum(N,M,K). 

prod(0,M,0). 
prod(s(N), M, P) :- 
    prod(N,M,K), 
    sum(K,M,P). 

我把乘法法則爲序言。然後我做查詢：

?- prod(X,Y,s(s(s(s(s(s(0))))))). 

這意味着基本上找到因子6。

以下是結果。

X = s(0), 
Y = s(s(s(s(s(s(0)))))) ? ; 
X = s(s(0)), 
Y = s(s(s(0))) ? ; 
X = s(s(s(0))), 
Y = s(s(0)) ? ; 
infinite loop 

該結果有兩個問題：

1. 並非所有的結果被示出，請注意，結果X = 6，Y = 1缺失。
2. 它不停止，除非我按Ctrl + C然後選擇中止。

所以...我的問題是：

1. 這是爲什麼？我嘗試過轉換「prod」和「sum」。由此產生的代碼給我所有的結果。而且，爲什麼呢？儘管如此，它仍然是死循環的。
2. 如何解決？

我讀了無限循環的其他答案。但我會很感激有人基於這種情況回答。它對我很有幫助。

Answer 1

如果你想深入研究終止性質，程序使用successor-arithmetics是一個理想的研究對象：你知道先驗他們應該說明，這樣你就可以專注於更多的技術細節。你需要了解幾個概念。

通用終止

最簡單的方法來解釋它，是考慮Goal, false。這終止如果Goal通用終止。那就是：查看跟蹤器是最無效的方法 - 它們只會向您顯示一條執行路徑。但是你需要立即理解所有這些！當你想要通用終止的時候也不要看答案，他們只會分散你的注意力。你已經看到它：你有三個整潔和正確的答案，只有當你的程序循環。所以更好地「關閉」與false答案。這消除了所有分心。

失敗切片

需要的下一個概念就是failure slice的。採取一個純粹的單調邏輯程序，並投入一些目標false。如果生成的失敗片沒有終止（普遍），原始程序也不會。在您爲例，考慮：

 
prod(0,M,0) :- false. 
prod(s(N), M, P) :- 
    prod(N,M,K), false, 
    sum(K,M,P). 

這些false目標，有助於消除在你的程序無關的裝飾品：剩餘部分顯示你清楚，爲什麼prod(X,Y,s(s(s(s(s(s(0))))))).不會終止。它不會終止，因爲該片段根本不在乎P！你希望第三個參數有助於終止prod/3，但是這個片段告訴你這全是徒勞的，因爲P不會出現在任何目標中。不需要聊天跟蹤器。

通常找到最小的故障切片並不是那麼容易。但是一旦你找到了一個，那麼確定它的終止或者非終止屬性是微不足道的。過了一段時間，你可以用你的直覺來想象一個切片，然後你可以用你的理由來檢查切片是否相關。

什麼是非常顯着的失敗片的概念是這樣的：如果你想改善程序，你必須修改你的程序在上面的片段中可見的部分！只要你不改變它，問題就會持續。故障切片因此是您程序中非常重要的部分。

終止推斷

這是你需要的最後一件事：一個終止inferencer（或分析器），如cTI將幫助您快速識別終止條件。看看prod/3的推斷終止條件和改進prod2/3here！

---

編輯：既然這是一個作業問題，我還沒有發佈最終的解決方案。但要清楚，這裏是到目前爲止所獲得的終止條件：

 
    prod(A,B,C)terminates_if b(A),b(B). 
    prod2(A,B,C)terminates_if b(A),b(B);b(A),b(C). 

所以新prod2/3嚴格比原來的方案更好！

現在，您需要找到最終的程序。其終止條件是：

 
    prod3(A,B,C)terminates_if b(A),b(B);b(C). 

首先，嘗試找到prod2(A,B,s(s(s(s(s(s(0)))))))的故障切片！我們預計它會終止，但它仍然不會。所以採取該程序並手動添加false目標！剩下的部分會告訴你關鍵！

作爲最後的提示：您需要添加一個額外的目標和一個事實。

---

編輯：根據要求，這裏是prod2(A,B,s(s(s(s(s(s(0)))))))失敗切片：

 
prod2(0,_,0) :- false. 
prod2(s(N), M, P) :- 
    sum(M, K, P), 
    prod2(N,M,K), false. 

sum(0, M, M). 
sum(s(N), M, s(K)) :- false, 
    sum(N,M,K). 

請注意，sum/3的顯著簡化定義。它只是說：0加上任何東西。不再。因此，即使更專業的prod2(A,0,s(s(s(s(s(s(0)))))))將循環，而prod2(0,X,Y)優雅地終止...

Answer 2

第一個問題（爲什麼）很容易發現，特別是如果知道left recursion。sum(A,B,C)綁定 A和B當C 是綁定，但原始程序prod（A，B，C）不使用該綁定，而是仍然遞歸與仍然A，B unbound。

如果我們換總和，督促我們從和2個有用綁定遞歸調用：

sum(M, K, P) 

現在M被裝訂成冊，將用於終止左遞歸。我們可以交換N和M，因爲我們知道產品是可交換的。

sum(0, M, M). 
sum(s(N), M, s(K)) :- 
    sum(N, M, K). 

prod3(0, _, 0). 
prod3(s(N), M, P) :- 
    sum(M, K, P), 
    prod3(M, N, K). 

注意，如果我們換M，K（即總和（K，M，P）），當prod3被稱爲以P未知，我們再有一個非終止循環，但總和。

?- prod3(X,Y,s(s(s(s(s(s(0))))))). 
X = s(s(s(s(s(s(0)))))), 
Y = s(0) ; 
X = s(s(s(0))), 
Y = s(s(0)) ; 
X = s(s(0)), 
Y = s(s(s(0))) ; 
X = s(0), 
Y = s(s(s(s(s(s(0)))))) ; 
false. 

OT我被CTI報告困擾：prod3（A，B，C）terminates_if B（A），B（B）; B（A），B（C）。