pattern-matching - 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) ; (not A, C) ，Mercury 的决定论推理通常不够聪明，无法找出相反的情况。

尤其是，Mercury 的决定论推断并没有试图从总体上确定两个子句是相互排斥的。在这种情况下，它知道 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 困住。