水星:确定性和模式匹配

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

是的，水星模式匹配的工作方式与SML不同。Mercury对其声明性语义非常严格。一个有多个从句的谓语相当于所有主体的析取(以小句中心统一的一些复杂性为模)，析取的含义不受析取的不同分支的书写顺序的影响。事实上，水星的含义很少受到编写顺序的影响(状态变量是我能想到的唯一例子)。

因此，如果不将N \= 0放入正文中，使用模式匹配的带有两个子句的谓词就是不确定性的。没有什么可以阻止nth(Tl, 0 - 1, X)成为nth([_ | Tl], 0, 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.

这称为交换机。编译器知道一个列表有两个构造函数(空的列表[]或cons单元格[|])，而给定的列表只能是其中之一，因此具有两个构造函数的arm的析取(或谓词的多个子句)必须是确定性的。如果一个析取(多个子句)包含一些但不是所有构造函数的case，那么它将被推断为半确定性的。

Mercury还能够为开关生成非常有效的代码，并且当你通过添加新的案例来改变类型时，还会通知你所有需要改变的地方，所以在可能的情况下使用开关被认为是一个很好的风格。然而，在像您这样的情况下，您不得不使用if/then/else。