“：=”和“==”在水星

Question

我最近在 Mercury 中看到了这个代码示例：

append(X,Y,Z) :-
  X == [],
  Z := Y.
append(X,Y,Z) :-
  X => [H | T],
  append(T,Y,NT),
  Z <= [H | NT].

作为一名 Prolog 程序员，我想知道：普通的统一 = 之间有什么区别 以及这里使用的 := 或 => ？

在 Mercury 参考< /a>，这些运算符获得不同的优先级，但他们没有解释其中的差异。

Answer 1

首先让我们使用缩进重新编写代码：

append(X, Y, Z) :-
    X == [],
    Z := Y.
append(X, Y, Z) :-
    X => [H | T],
    append(T, Y, NT),
    Z <= [H | NT].

您似乎必须将所有代码缩进四个空格，这在注释中似乎不起作用，我上面的注释应该被忽略（我无法删除它们）。

上面的代码不是真正的 Mercury 代码，而是伪代码。它作为真正的 Mercury 代码没有意义，因为 <= 和 => 运算符用于类型类 (IIRC)，而不是统一。另外，我以前没有见过 := 运算符，我不确定它的作用。

在这种伪代码风格中（我相信），作者试图表明 := 是统一的赋值类型，其中 X 是分配了值Y。类似地，=> 显示 X 的解构，<= 显示构造< /em> 的 Z。另外 == 显示 X 和空列表之间的相等测试。所有这些操作都是统一的类型。编译器知道谓词的每种模式应该使用哪种类型的统一。对于此代码，有意义的模式是 append(in, in, out)

Mercury 在这方面与 Prolog 不同，它知道要使用哪种类型的统一，因此可以生成更高效的代码并确保该程序模式正确。

还有一件事，此伪代码的真实 Mercury 代码将是：

:- pred append(list(T)::in, list(T)::in, list(T)::out) is det.

append(X, Y, Z) :-
    X = [],
    Z = Y.
append(X, Y, Z) :-
    X = [H | T],
    append(T, Y, NT),
    Z = [H | NT].

请注意，每个统一都是 = 并且已添加谓词和模式声明。

Answer 2

在具体的 Mercury 语法中，运算符 := 用于字段更新。

Answer 3

也许我们无法使用像 ':=' '<=' '=>' 这样的运算符最近的 Mercury 版本中出现了 '=='，但根据 Nancy Mazur 论文中的描述，实际上这些运算符是专门化的统一。
'=>'代表解构，例如 X => f(Y1, Y2, ..., Yn)，其中 X 为输入，所有 Yn 为输出。这是半德特。 '<=' 则相反，并且是 det。 '=='用于两边都磨的情况，是semidet。 ':=' 就像任何其他语言中的常规赋值运算符一样，并且它是 det。在较旧的论文中，我什至看到他们使用“==”而不是“=>”执行解构。 （我觉得我的英语很糟糕=x=）