每日彙整: 2015-07-10

樹莓派、樹莓派之學習、樹莓派之教育

勇闖新世界︰ 《 pyDatalog 》 導引《六》

既然『pyDatalog』的推論引擎是用『SLDNF』 ── SLD resolution with Negation as Failure ── ，對此有個清清楚楚的了解就顯得十分重要了。首先引用

《 Simply Logical
Intelligent Reasoning by Example 》

3.1 SLD-resolution

Prolog’s proof procedure is based on resolution refutation in definite clause logic. Resolution refutation has been explained in the previous chapter. In order to turn it into an executable proof procedure, we have to specify how a literal to resolve upon is selected, and how the second input clause is found. Jointly, this is called a resolution strategy. Consider the following program:

student_of(X,T):-follows(X,C),teaches(T,C).
follows(paul,computer_science).
follows(paul,expert_systems).
follows(maria,ai_techniques).
teaches(adrian,expert_systems).
teaches(peter,ai_techniques).
teaches(peter,computer_science).

The query ?-student_of(S,peter) has two possible answers: {S → paul} and {S → maria}. In order to find these answers, we first resolve the query with the first clause, yielding

:-follows(S,C),teaches(peter,C)

Now we have to decide whether we will search for a clause which resolves on follows(S,C), or for a clause which resolves on teaches(peter,C). This decision is governed by a selection rule. Prolog’s selection rule is left to right, thus Prolog will search for a clause with a positive literal unifying with follows(S,C). There are three of these, so now we must decide which one to try first. Prolog searches the clauses in the program top-down, so Prolog finds the answer {S → paul} first. Note that the second choice leads to a dead end: the resolvent is

:-teaches(peter,expert_systems)

which doesn’t resolve with any clause in the program.

This process is called SLD-resolution: S for selection rule, L for linear resolution (which refers to the shape of the proof trees obtained), and D for definite clauses. Graphically, SLD-resolution can be depicted as in fig. 3.1. This SLD-tree should not be confused with a proof tree: first, only the resolvents are shown (no input clauses or unifiers), and second, it contains every possible resolution step. Thus, every leaf of an SLD-tree which contains the empty clause corresponds to a refutation and hence to a proof tree; such a leaf
is also called a success branch. An underlined leaf which does not contain □ represents a failure branch.

SLD-treeAs remarked already, Prolog searches the clauses in the program top-down, which is the same as traversing the SLD-tree from left to right. This not only determines the order in which answers (i.e. success branches) are found: it also determines whether any answers are found at all, because an SLD-tree may contain infinite branches, if some predicates in the program are recursive. As an example, consider the following program:

brother_of(X,Y):-brother_of(Y,X).
brother_of(paul,peter).

An SLD-tree for the query ?-brother_of(peter,B) is depicted in fig. 3.2. If we descend this tree taking the left branch at every node, we will never reach a leaf. On the other hand, if we take the right branch at every node, we almost immediately reach a success branch. Taking right branches instead of left branches in an SLD-tree corresponds to
searching the clauses from bottom to top. The same effect would be obtained by reversing the order of the clauses in the program, and the SLD-tree clearly shows that this is enough to prevent Prolog from looping on this query. This is a rule of thumb that applies to most cases: put non-recursive clauses before recursive ones.
SLD-Tree-∞

在此如果參照

《 λ 運算︰概念導引《四》》文本中

『 λ表達式』的求值策略 ── \beta 化約 ── ，將能對『不同』的抽象系統論述都有更深之認識。畢竟『理則』是『無處不在』的吧！

假使說給定了一個『 λ表達式』 (\lambda x. ((\lambda y. (x \ y)) \ \Box) \ \bigcirc)，有人『第一步』這樣作『 \beta 化約』︰

((\lambda y. ( \bigcirc \ y)) \ \Box )

，也有人『第一步』這樣作『 \beta 化約』︰

(\lambda x. ( (x \ \Box ) \ \bigcirc)

，這樣不同的『步驟選擇』是否會產生『不同結果』的呢？如果說再次繼續進行『 \beta 化約』，兩者都會得到︰

(\bigcirc \ \Box )

，於是我們就可以歸結的說『 \beta 化約』不管是用著怎麽樣的『步驟次序』，都一定能夠得到『相同結果』的嗎？？

為了考察不同次序步驟的『化約策略』，首先讓我們定義『單步 \beta 化約』︰

A \equiv_{\beta^1} B

是指表達式 B 是經由表達式 A 中的某一函式應用子表達式 C =_{df} ((\lambda x. M) N) 『 \beta 化約』而得來。假使『約定』零步 \beta 化約是說 『A \equiv_{\beta^0} A』，這樣我們就可以說『單步』或『多次單步』之『單步 \beta 化約』的『化約封閉性』︰

U \equiv_{\beta^*} V

，是講存在一個『單步 \beta 化約』的『序列』

U =_{df} S_1, S_2, S_3, \cdots, S_k, S_{k+1}, \cdots, S_n =_{df} V, \ S_k \equiv_{\beta^1} S_{k+1}, k=1\cdots n

。某一表達式 U 我們稱它是『 \beta 可化約』\beta-redex 是指這個表達式還有『未化約』的子應用表達式 ((\lambda x. M) N) 。如果經過『有限的』化約序列，最終抵達一個『沒有未化約』的表達式 V，也就是說 V 中沒有 \beta-redex，這時我們將 V 稱之為『 \beta 正規元型』normal form。於是我們就可以問︰

各種不同的『化約序列』如果存在『 \beta 正規元型』，那它們是相同的嗎？

【Church-Rosser 定理】說

如果 P \equiv_{\beta^*} Q 而且 P \equiv_{\beta^*} R；那麼就會存在一個 S， 使得 Q \equiv_{\beta^*} S 以及 R \equiv_{\beta^*} S。

所以可以講不同的『化約序列』之『 \beta 正規元型』，除了其內函式中的『受約束變元』之『虛名』不同外 ── 可以作『 \alpha 變換』使之一樣 ──，都是『相同的』。這是一個非常重要的歸結，設想萬一它不是這樣，那所謂的『計算』不就成『笑話』了嗎！然而需要小心的是『 \beta 化約』是『單行道』，也就是說 A \equiv_{\beta} B 成立，並不代表 B \equiv_{\beta} A 正確。比方講 ((\lambda x. x) a) \equiv_{\beta} a，從結果變元 a 又要怎麼得回原來函式應用的呢？

那麼『 \beta 化約策略』Reduction Strategy 又是什麼呢？它是一個『函式』RS，可以定義如下︰

一、『定義域』與『對應域』是『所有的 λ 表達式』構成的集合

二、如果 e 是一個『 \beta 正規元型』，RS(e) = e

三、假使 m 不是『 \beta 正規元型』，化約策略會依據特定方式選擇 m 中的某一『優先』 \beta-redex 子表達項 t，RS(m) = t

這樣看來 RS 函式選擇了特定的『步驟次序』── 策略 ── 來作『單步 \beta 化約』，這也是『程式』之『最佳化』optimize 的源起。然而不是每種『化約策略』都能夠抵達存在的『 \beta 正規元型』。舉例說兩種簡單的『左』和『右』化約策略，它總是優先選擇表達式中的『最左』與『最右』 \beta-redex 子表達項 。

TIW

考慮用『左右』策略化約下面的表達式

(((\lambda x. (\lambda y. x)) (\lambda z. z)) (\lambda w. (w w)))

。

用『左』策略會得到『上圖』，用『右』策略會卡在 (\lambda w. (w w))。

所謂的『正規策略』是說用這個策略能夠得到『所有可能存在的』 \beta 正規元型。事實上從邏輯推理可以證明『最左優先』策略是一種『正則策略』，果真是『天左旋』的乎！！

……

然而『Datalog』宣稱自己是『純陳述』的『邏輯編程』語言，

Datalog is a truly declarative logic programming language that syntactically is a subset of Prolog. It is often used as a query language for deductive databases. In recent years, Datalog has found new application in data integration, information extraction, networking, program analysis, security, and cloud computing.

『pyDatalog』對它做了繼承與擴張，它是否具有『純陳述』特性，可以不用管『陳述次序』的呢？僅從

Reference

  • although the order of pyDatalog statements is indifferent (except for functions), the order of literals within a body is significant:
  • an expression used as the argument of a logic function must be  bound by a previous literal (otherwise no result is returned)
  • the right hand side of X==expr must be bound by a previous literal (otherwise, no result is returned)
  • the right hand side of p[X]< expr must be bound (otherwise, no result is returned).
  • the left and right hand sides of  expr1 < expr2 comparisons must be bound (otherwise, an error is raised)

說明就可以『推測』結論，有興趣的讀者將底下的程式中

 

pi@raspberrypi ~ $ python3
Python 3.2.3 (default, Mar  1 2013, 11:53:50) 
[GCC 4.6.3] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from pyDatalog import pyDatalog
>>> pyDatalog.create_terms('X單位, Y單位, Z單位, V數值, 單位轉換, 重量轉換')
>>> 單位轉換['公斤', '公克'] = 1000
>>> 單位轉換['台斤', '公克'] = 600
>>> 單位轉換['市斤', '公克'] = 500
>>> 單位轉換['英磅', '公克'] = 453.59237
>>> 單位轉換[X單位, Y單位] = 單位轉換[X單位, Z單位] * 單位轉換[Z單位, Y單位]
>>> 單位轉換[X單位, Y單位] = 1 / 單位轉換[Y單位, X單位]
>>> print(單位轉換['公斤', '台斤'] == V數值)
V數值               
------------------
1.6666666666666667
>>> print(單位轉換['英磅', '台斤'] == V數值)
V數值               
------------------
0.7559872833333334
>>> 單位轉換['台斤', '台兩'] = 16
>>> 重量轉換[V數值, X單位, Y單位] = V數值 * 單位轉換[X單位, Y單位]
>>> print(重量轉換[1, '公斤', '台兩'] == V數值)
V數值               
------------------
26.666666666666668
>>>

 

這兩行互換

‧ 單位轉換[X單位, Y單位] = 單位轉換[X單位, Z單位] * 單位轉換[Z單位, Y單位]

‧ 單位轉換[X單位, Y單位] = 1 / 單位轉換[Y單位, X單位]

，自行探究看看會發生什麼事情？

邏輯『易知難通』，通常是因為人腦不像電腦，可以『逐字逐句』不厭其煩之『一行一行』的讀解，『一遍一遍』的重複，所以容易漏掉許多重要或不重要事項，最後推理錯誤，大概也不必太驚訝的吧！不過那個推論引擎『目前』還是人類創作的哩！！