Mercury：决定论和模式匹配

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。 Mercury 的工作方式是否有所不同？即使 N 为 0，情况 B 也会被调用吗？ （我在情况 B 中添加了 N \= 0 子句，希望使谓词成为半确定性的，但这并不起作用。）

有没有一种方法可以使用半确定性的模式匹配来编写此谓词？

Answer 1

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

因此，如果不将 N \= 0 放入正文中，则使用模式匹配的两个子句的谓词是不确定的。没有什么可以阻止 nth(Tl, 0 - 1, X) 成为 nth([_ | Tl], 0, X) 的有效约简。

有了 N \= 0，您就走上了正确的道路。不幸的是，虽然 if A then B else C 逻辑上等同于 (A, B) ； （不是 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 单元 [|]），并且给定列表只能是其中之一，因此，具有两个构造函数的分支的析取（或谓词的多个子句）必须是确定性的。对于某些但不是全部构造函数的情况的析取（多个子句）将被推断为半确定性的。

Mercury 还能够为开关生成非常高效的代码，并且当您通过添加新案例更改类型时，还会通知您所有需要更改的地方，因此尽可能使用开关被认为是良好的风格。然而，在像您这样的情况下，您会陷入 if/then/else 的困境。