水星中的":=“和"=>”

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 reference中，这些运算符具有不同的优先级，但它们不能解释这种差异。

Answer 1

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

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

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

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

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

水星在这方面不同于Prolog，它知道使用哪种类型的统一，因此可以生成更有效的代码，并确保程序是模式正确的。

还有一件事，这个伪代码的真正的墨丘利代码是：

:- 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

也许我们不能在最近的水星版本中使用像':=‘，'<=’，'=>‘，'==’这样的运算符，但实际上，根据南希·马祖尔的论文中的描述，这些运算符是专门统一的。' =>‘代表解构，例如X=> f(Y1，Y2，...，Yn)，其中X是输入，所有Yn是输出。这是半圆的。'<=‘正好相反，它是det。'==‘用于两边都是地面的情况，它是半形的。':=‘就像任何其他语言中的常规赋值运算符，它是det。在以前的论文中，我甚至看到他们使用“==”而不是“=>”来执行解构。(我觉得我的英语很糟糕=x =)