SWI-Prolog谓词

Question

我对prolog非常陌生，我的教授似乎忘记了教授课程的基本用法。他给我们写谓词stmt是和支杆的任务，与第一断言看起来像：

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

，然后通过测试代码语句（[用法，X，东西，否则]，[什么东西，别的]） 。

第二部分如下所示：

定义一个撑条谓词使得{stmts(List1, List2)}是可证明如果(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是“未证实的变量”。

如果我们结合这两个我们可以看到，脱你的代码的变种是：

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不能统一。第一个条款“失败”。

In Prolog a backtracking机制已到位：在调用第一个子句之后 - 无论这是成功还是失败 - 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)是一个内建的，并成功（我们不打算再次在这里做统一过程）。这意味着第三个条款成功了。