水星:决定论和模式匹配

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也可以被调用吗？(我将N \= 0条款添加到案例B中,希望使谓词半自由,但这不起作用.)

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

Answer 1

是的,Mercury模式匹配与SML的工作方式不同.水星对其声明性语义非常严格.具有多个子句的谓词相当于所有实体的分离(以子句头中的统一为模的一些并发症),并且分离的含义不受分离的不同分支的顺序的影响.事实上,很少有水星的意义受你写东西的影响(状态变量是我能想到的唯一例子).

因此,如果没有放入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的析取(或谓词的多个子句)必须是确定性的.具有一些但不是所有构造函数的情况的析取(多个子句)将被推断为半确定性的.

Mercury还能够为交换机生成非常高效的代码,并且还可以通过添加新案例来通知您在更改类型时需要更改的所有位置,因此在可能的情况下使用交换机被认为是好的方式.在像你这样的情况下,你会遇到if/then/else.