什麼是後繼算術總和的最佳綠色切割？

Question

在Prolog中討論綠色切割我試圖在後續算法中將它們添加到sum的標準定義中（請參見What's the SLD tree for this query?中的謂詞plus）。這個想法是通過消除所有無用的回溯（即沒有0​​）來儘可能地「清理」輸出，同時在所有可能的參數實例化組合中保持相同的行爲 - 所有實例化的，一/二/三個完全沒有實例化的，以及所有包括部分實例化參數的變體。

這就是我能夠同時努力來儘可能接近這個理想（我承認錯誤的答案how to insert green cuts into append/3作爲源）做：

natural_number(0). 
natural_number(s(X)) :- natural_number(X). 

plus(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), natural_number(X). 
plus(X, s(Y), s(Z)) :- plus(X, Y, Z). 

在SWI這似乎工作的優良除?- plus(+X, -Y, +Z).外的所有查詢，SWI's notation of predicate description。例如，?- plus(s(s(0)), Y, s(s(s(0)))).產生Y = s(0) ; false.。我的問題是：

• 我們如何證明上述削減是（或不是）綠色？
• 我們能否比上述節目做得更好，並且通過增加一些其他綠色減少來消除最後的回溯？
• 如果是，如何？

Answer 1

首先是一個小問題：plus/3的通用定義具有交換的第一個和第二個參數，允許利用第一個參數的索引。參見序言藝術的程序3.3。這也應該在你的previous post中改變。我會打電話給您的交換定義plusp/3和您的優化定義pluspo/3。因此，鑑於

 
plusp(X, 0, X) :- natural_number(X). 
plusp(X, s(Y), s(Z)) :- plusp(X, Y, Z). 

檢測紅色切口（問題一）

如何證明或反駁紅/綠削減？首先，留意警衛隊的「寫」 - 日程。也就是說，對於任何此類統一之前的裁員。在您的優化方案：

pluspo(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), ...

我發現以下幾點：

pluspo(X, Y, X) :- (...... ->! ; ...), ...

所以，讓我們建立一個反例：要以紅色的方式進行剪切，「寫入統一」必須使其實際後衛Y == 0爲真。這意味着構建的目標必須以某種方式包含常量0。只有兩種可能性需要考慮。第一個或第三個參數。最後一個參數中的零意味着我們至多有一個解決方案，因此不可能削減更多的解決方案。所以，0必須在第一個參數！ （第二個參數從一開始就不能是0，或者「寫統一不會產生不利影響。」）。以下是一個這樣的反：

?- pluspo(0, Y, Y).

其給出一個正確的解Y = 0，但是隱藏了所有其他的人！所以在這裏我們有這樣一個邪惡的紅色切割！ 它對比的未經優化的程序，它給了無窮多解：

 
Y = 0 ; 
Y = s(0) ; 
Y = s(s(0)) ; 
Y = s(s(s(0))) ; 
... 

所以，你的程序是不完整的，並且關於進一步優化它的任何問題，因此是不相關的。但是，我們可以做的更好，讓我重申，我們要優化的實際定義：

 
plus(0, X, X) :- natural_number(X). 
plus(s(X), Y, s(Z)) :- plus(X, Y, Z). 

在幾乎所有的Prolog系統來說，首先是參數的索引，這使得下面的查詢確定的：

 
?- plus(s(0),0,X). 
X = s(0). 

但許多系統不支持（完整）第三個參數索引。因此，我們得到SWI，YAP，SICStus：

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

什麼你可能想要寫的是：

 
pluso(X, Y, Z) :- 
    % Part one: green cuts 
    ( X == 0 -> ! % first-argument indexing 
    ; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe 
    ; true 
    ), 
    % Part two: the original unifications 
    X = 0, 
    Y = Z, 
    natural_number(Z). 
pluso(s(X), Y, s(Z)) :- pluso(X, Y, Z). 

注意差異pluspo/3：現在只有測試之前，切！此後所有的統一。

 
?- pluso(X, Y, 0). 
X = Y, Y = 0. 

迄今爲止的優化只依靠調查兩個子句的頭部。他們沒有考慮到遞歸規則。因此，它們可以在沒有任何全局分析的情況下整合到Prolog編譯器中。在O'Keefe的術語中，這些綠色切割可能被認爲是藍色切割。舉The Craft of Prolog，3.12：

藍削減在那裏，提醒Prolog的系統，它應該已經注意到確定性，但不會。藍色切割不會改變程序的可見行爲：他們所做的一切都是可行的。

綠色削減在那裏精簡掉試圖證明這會成功或者是無關緊要的，或將註定要失敗的，但你不希望Prolog的系統能夠告訴。

但是，最重要的是這些切割確實需要一些警衛才能正常工作。現在

，你考慮的另一個查詢：

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

或把一個簡單的情況：

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

這裏，頭都適用，因此係統不能夠確定決定。然而，我們知道目標plus(X, s^n, s^m)與n>m沒有解決方案。所以通過考慮plus/3的模型，我們可以進一步避免選擇點。我會馬上回來：

---

更好地使用call_semidet/1！

它變得越來越複雜，有可能優化可能會輕易地在程序中引入新的錯誤。另外優化的程序是維護的噩夢。爲了實際編程目的，使用call_semidet/1。這是安全的，並且如果你的假設是錯誤的，將會產生一個乾淨的錯誤。

---

返回商業：這是一個進一步的優化。如果Y和Z是相同的，第二條可以不適用：

 
pluso2(X, Y, Z) :- 
    % Part one: green cuts 
    ( X == 0 -> ! % first-argument indexing 
    ; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe 
    ; Y == Z, ground(Z) -> ! 
    ; true 
    ), 
    % Part two: the original unifications 
    X = 0, 
    Y = Z, 
    natural_number(Z). 
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z). 

我（目前）認爲，pluso2/3是綠/藍裁員的最佳使用w.r.t.剩餘的選擇點。你要求證明。那麼，我認爲這是遠遠超出了答案...

目標ground(Z)是必要的，以確保非終止屬性。目標plus(s(_), Z, Z)不終止，該屬性由ground(Z)保留。也許你認爲這是一個好主意，也可以刪除無限的失敗分支？根據我的經驗，這是相當有問題的。特別是，如果這些分支被自動刪除。雖然乍一看似乎是個好主意，但它使得程序開發變得更加脆弱：另外一個良性的程序變更現在可能會禁用優化，從而「導致」未終止。但無論如何，在這裏我們去：

除了簡單的綠色削減

 
pluso3(X, Y, Z) :- 
    % Part one: green cuts 
    ( X == 0 -> ! % first-argument indexing 
    ; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe 
    ; Y == Z -> ! 
    ; var(Z), nonvar(Y), \+ unify_with_occurs_check(Z, Y) -> !, fail 
    ; var(Z), nonvar(X), \+ unify_with_occurs_check(Z, X) -> !, fail 
    ; true 
    ), 
    % Part two: the original unifications 
    X = 0, 
    Y = Z, 
    natural_number(Z). 
pluso3(s(X), Y, s(Z)) :- pluso3(X, Y, Z). 

，你可以在其中找到pluso3/3同時也有有限個答案不終止的情況下？