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)是一個內建的，併成功（我們不打算再次在這裏做統一過程）。這意味着第三個條款成功了。