水星：決定論和模式匹配

Question

我有一個半決定論的函數。當我重寫它來使用模式匹配而不是if語句時，Mercury說它變得不確定。我想明白爲什麼。

原始代碼：

:- pred nth(list(T), int, T). 
:- mode nth(in,  in, out) is semidet. 
nth([Hd | Tl], N, X) :- (if N = 0 then X = Hd else nth(Tl, N - 1, X)). 

修改後的代碼：

:- pred nth(list(T), int, T). 
:- mode nth(in,  in, out) is nondet. 
nth([Hd | _], 0, Hd).        % Case A 
nth([_ | Tl], N, X) :- N \= 0, nth(Tl, N - 1, X). % Case B 

我習慣考慮圖案在SML，匹配其中在情況A 0將確保在情況B中，N不是0.水星的工作方式不同嗎？即使N是0，情況B是否會被調用？ （我在案例B中添加了N \= 0子句，希望能夠使謂詞半決定論，但是這不起作用。）

有沒有辦法用模式匹配來寫這個謂詞也是半決定論的？

Answer 1

是的，Mercury模式匹配對SML的工作方式不同。水星對其聲明性語義非常嚴格。一個含有多個子句的謂詞等價於所有物體的分離（在子句頭中統一了一些複雜性），並且分離的含義不受寫入分離的不同臂的順序的影響。事實上Mercury中很少有它的含義受你寫的東西的影響（狀態變量是我能想到的唯一例子）。

因此，如果不將N \= 0置於正文中，那麼使用模式匹配的兩個子句的謂詞是非確定性。有沒有什麼可以阻止有效減少nth(Tl, 0 - 1, X)。

隨着N \= 0，你正在走上正軌。不幸的是，雖然if A then B else C是邏輯相當於(A, B) ; (not A, C)，但水星的確定性推論通常不夠聰明，以找出相反的結果。

特別是，水星的決定論推論並不試圖弄清楚兩個條款是相互排斥的。在這種情況下，它知道N = 0可以成功或失敗，具體取決於N的值，並且N \= 0可以成功或失敗，具體取決於N的值。既然它看到謂詞成功的兩種不同方式，並且可能失敗，它必定是非確定性的。有許多方法可以保證編譯器不會推斷它，但在這種情況下，只需堅持使用if/then/else就更容易。

可以使用而沒有編譯器的模式匹配的情況下，你可以有多個解決方案，當你將一個變量與幾個不同的相同類型的構造器進行匹配時。例如：

:- pred some_pred(list[T]) is det. 
some_pred([]) :- something. 
some_pred([H | T]) :- something_else. 

這被稱爲開關。編譯器知道一個列表有兩個構造函數（空列表[]或缺陷單元[|]），並且給定的列表只能是其中的一個，所以一個分支（或謂詞的多個子句）建設者必須是確定性的。對於一些但不是全部構造函數的情況的析取（多個子句）將被推斷爲半確定性的。

Mercury還能夠爲開關生成非常高效的代碼，並且通過添加新案例來更改類型時也會通知所有需要更改的位置，因此在可能的情況下使用開關被認爲是很好的風格。然而，在像你這樣的情況下，你被if/then/else困住了。