SWI-Prolog 谓词

Question

我对 prolog 很陌生，我的教授似乎忘记了教课程的基本用法。他给了我们编写谓词 stmt 和 stmts 的任务，第一个谓词看起来像：

stmt([pass|X], X).
stmt([declare,N|X], X) :- atom(N).
stmt([use,N|X], X) :- atom(N).

然后通过测试代码stmt([use,x,something,else],[something,else])。

第二部分如下所示：

定义一个 stmts 谓词，如果 (List1) 以匹配 (stmts) 非终结符的原子开始，然后以 List2 中的原子继续，则 {stmts(List1, List2)} 是可证明的。例如，以下查询应产生 true： stmts([pass,use,x,more,stuff],[more,stuff]).

我不明白如何让它发挥作用。任何帮助将不胜感激。

Answer 1

由于 Prolog 中的统一过程以及 Prolog 中的列表是 链表这一事实，它可以工作。

首先，了解列表是在CONS-way 中实现的可能很有用（如果我没记错的话，这个术语起源于 Lisp）。这意味着有一个函子（为简单起见，我们在这里使用cons/2），这样一个列表[use,x,something,else] 的结构类似于cons(use,cons(x,cons(something,cons(else,nil))))（nil 是列表的末尾）。所以以链表的方式。

接下来如果你“在 Prolog 中调用谓词”统一就会发生。它旨在将调用中的参数与子句头部的参数统一起来。例如，如果子句的头部是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))). 就会发生统一。 First 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))）。所以现在统一已经成功了，万岁。但我们还没有。现在第三个子句的 head 已经成功，这意味着我们现在必须对该子句的 body 执行调用。所以我们称之为：

atom(N).

由于N = x，这意味着我们调用x。现在atom(x) 是一个内置函数，并且成功了（我们不会在这里再次进行统一过程）。所以这意味着第三个子句成功了。