问SWI-Prolog谓词

EN

它的工作是因为Prolog中的统一过程以及Prolog中的列表是一个链接列表的事实。

首先，理解列表是在反方向中实现的(如果我没有记错的话，这个术语来自Lisp )，这一点可能很有用。这意味着有一个函子(为了简单起见，这里我们使用cons/2 )，这样的话，[use,x,something,else]的结构就像cons(use,cons(x,cons(something,cons(else,nil)))) (nil是列表的末尾)。所以以链接列表的方式。

接下来，如果您“在Prolog中调用谓词”，则会发生统一。它的目的是将调用中的论点与条款头中的论点统一起来。例如，如果claus的头是foo(bar(X,qux(Y)))，而您用foo(bar(3,Z))调用它，那么结果是X = 3和Z = qux(Y)，X和Y是“未实例化的变量”。

如果我们将这两者结合在一起，我们就会看到代码的一个desugared变体是：

stmt(cons(pass,X), X).
stmt(cons(declare,cons(N,X)), X) :- atom(N).
stmt(cons(use,cons(N,X)), X) :- atom(N).

所以现在，如果我们称之为stmt(cons(use,cons(x,cons(something,cons(else,nil)))),cons(something,cons(else,nil))).，统一就会发生。第一个Prolog旨在与第一个条款相统一：

stmt(cons(pass,X),         X)
stmt(cons(use, cons(x,...),cons(something,cons(else,nil)))

(我用椭圆来保持简单)。

统一的目的是统一第一个论点，例如：

cons(pass,X) ~ cons(use,cons(else,...))
X ~ cons(something,cons(else,nil))

现在统一将剥离:删除第一个统一，并注入统一的参数，因此：

pass ~ use
X ~ cons(else,...)
X ~ cons(something,cons(else,nil))

现在，在Prolog中，pass和use是常量(因为它们以小写开头)。此外，Prolog中的所有常量都是不同的(除非名称相同)。所以既然pass ~ use不能统一。第一句“失败”。

在Prolog中，有一个回溯机制:在调用第一个子句之后--无论这是成功还是失败-- Prolog将使用第二个子句、第三个子句等重试调用。

所以现在我们的目标是统一号召。所以现在我们进行统一，就像：

stmt(cons(declare,cons(N,X  )),X)
stmt(cons(use,    cons(x,...)),cons(something,cons(else,nil)))

导致统一的结果就像：

cons(declare,cons(N,X)) ~ cons(use,cons(x,...))
X ~ cons(something,cons(else,nil))

我们再一次剥皮

declare ~ use
cons(N,X) ~ cons(x,...)
X ~ cons(something,cons(else,nil))

再说一次，这是个失败。

我们的最后尝试是：

stmt(cons(use,cons(N,X)) ,X).
stmt(cons(use,cons(x,...),cons(something,cons(else,nil)))

产生的结果：

cons(use,cons(N,X)) ~ cons(use,cons(x,...))
X ~ cons(something,cons(else,nil))

然后产生：

use ~ use
cons(N,X) ~ cons(x,...)
X ~ cons(something,cons(else,nil))

其结果是：

use ~ use
N ~ x
X ~ ...
X ~ cons(something,cons(else,nil))

( ...是cons(something,cons(else,nil)))。所以现在统一成功了，欢呼。但我们还没到。现在，第三个子句的标题成功了，这意味着我们现在必须对该子句的主体执行调用。所以我们呼吁：

atom(N).

从N = x开始，这意味着我们打电话给x。现在，atom(x)是一个内置的，并且成功了(我们不打算在这里再次完成统一过程)。这就意味着第三条条款成功了。