4

我有一个半确定性的功能。当我重写它以使用模式匹配而不是 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 也会被调用吗？（我在N \= 0案例 B 中添加了该子句，希望使谓词具有半确定性，但这没有用。）

有没有办法用也是半确定性的模式匹配来编写这个谓词？

4

1 回答 1

8

是的，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可以成功或失败。由于它看到谓词成功的两种不同方式，并且它可能失败，因此它必须是不确定的。有一些方法可以向编译器保证确定性不是它会推断的，但在这种情况下，坚持使用 if/then/else 会更容易。N \= 0N

当您将单个变量与多个相同类型的不同构造函数匹配时，您可以使用模式匹配而编译器不会认为您可以有多个解决方案。例如：

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

这称为开关。编译器知道一个列表有两个构造函数（空列表[]或 cons 单元格[|]），并且给定的列表只能是其中之一，因此对于两个构造函数都有一个分支的析取（或谓词的多个子句）必须是确定性的。带有某些但不是所有构造函数的情况的析取（多个子句）将被推断为半确定性的。

Mercury 还能够为开关生成非常有效的代码，并且还可以在您通过添加新案例更改类型时通知您所有需要更改的地方，因此在可能的情况下使用开关被认为是一种很好的风格。但是，在像您这样的情况下，您会遇到 if/then/else。

于 2011-09-19T06:37:44.590 回答