邏輯式編程語言極簡實現（使用C#） - 3. 運行原理

本系列前面的文章：

• 邏輯式編程語言極簡實現（使用C#） - 1. 邏輯式編程語言介紹
• 邏輯式編程語言極簡實現（使用C#） - 2. 一道邏輯題：誰是兇手

次日，好爲人師的老明繼續開講他的私人課堂。

「今天講NMiniKanren的運行原理。」老明敲了敲白板，開始塗畫代碼，「咱們從一個喜聞樂見的例子開始。」

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.Any(k.Eq(x, 1), k.Eq(x, 2)),
        k.Any(k.Eq(y, x), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));

「這題我會了！」小皮在例子下邊寫下答案：

[(1 1), (1 b), (2 2), (2 b)]

看到小皮沒把昨天的知識忘光，老明略感欣慰：「不錯。你這個答案是怎麼算出來的呢？」

「呃……就是那個……」小皮突然卡殼了。這種問題就比如幾何證實題，明明一眼就能看出來的兩條垂直線，真下手證實卻發現還挺不容易。小皮抓了幾把頭髮，總算理出一縷思緒：「大概就是找出全部條件可能的組合……而後算一下解……」小皮一邊說，一邊在白板上寫着：

• x == 1
  • y == x => (x y) == (1 1)
  • y == "b" => (x y) == (1 "b")
• x == 2
  • y == x => (x y) == (2 2)
  • y == "b" => (x y) == (2 "b")

「嗯，其實你已經知道怎麼算出答案來了。只是對於其中的細節還不甚明瞭。咱們接下來要作的事要理清楚這個計算過程，獲得一個每一步均可以由計算機明確執行的算法。

「這個算法其實就是你所說這樣，找出全部可能的條件組合。每組條件組合能夠求出一個解，也可能自相矛盾從而無解。因爲NMiniKanren中的條件都是相等條件，因此一組條件組合能夠看做一個替換（Substitution）。一個替換能產生一個解，或者無解。

「所以，只需解決下面兩個問題：

1. 要在什麼數據結構上按照什麼順序遍歷替換。
2. 如何從替換中算出一個解，或者判斷其無解。」

遍歷分支

首先，咱們要從代碼構造出一個數據結構（其實就是一張圖）。這個數據結構可以按照必定的順序進行遍歷，並依次生成替換。

例子中的代碼使用到了Eq、Any和All這三種構造目標的方法。下面分別探討怎樣從這三種方法構造出咱們須要的數據結構來。

Eq

「k.Eq(a, b)構造的目標是什麼意思呢？」老明以一個看似平凡的問題開頭。

「簡單，意思就是a要等於b這個條件。」

「孤立地看，是這樣。可是考慮到上下文，更精確地說應該是，在上下文的基礎上追加a等於b這個條件。」

小皮有點不解：「emm……多了‘追加’有什麼不一樣呢？」

「從文字上看，多了‘追加’後，目標的解釋從一種名詞（一組條件）變成了動詞（追加條件）。這樣一來，目標不只表達了一組條件，同時也表達了這些條件如何跟上下文結合。就Eq的狀況來講，這個結合方式是‘追加’。而Any和All會有其餘結合方式。」

「雖然還不是很明白，我想這個要等Any和All的狀況一塊兒對比才能清晰起來。我還另外有個問題，上下文指的是什麼？」

「狹義地說，上下文是解釋器運行到這一條代碼時，已執行的代碼生成的替換。

上下文 <-> 一個替換 <-> 一組條件

「廣義上看，上下文還應該包含回溯分支等控制信息，不過目前咱們先忽略這些。

「綜合起來，按照對Eq目標的解釋，咱們能夠用下圖來表示這個目標。」

Any（或）

「接着看Any。按照上面的討論，咱們要怎麼解釋Any目標呢？」老明繼續發問。

「解釋目標要說清楚兩個方面：名詞（什麼條件）和動詞（如何與上下文結合）。以一開始的例子中的k.Any(k.Eq(x, 1), k.Eq(x, 2))爲例。名詞方面天然就是x等於1和x等於2兩個條件了，不過這兩個條件是‘或’的關係。動詞方面，應該是從上下文分岔出兩個分支，一個分支追加x等於1這個條件，另外一個分支追加x等於2這個條件。」

「很好。也就是說，和Eq不一樣，Any操做和上下文結合後，會生成多個替換。」老明讚許地點點頭，「它把參數的分支都放在一塊兒，就像加法似的。用圖表示的話，就像下面這樣。」

All（與）

「最後是All……」

「這個我也會了！」小皮打斷老明，「k.All(a, b)名詞上表示條件a且條件b；動詞上表示上下文先追加a，再追加b。」

「你說的太籠統了。a和b可能都有多個分支，這種狀況下怎麼作？」老明接着問道。

小皮想了想一開始作的例子，答道：「這種狀況要取全部組合，也就是a的分支和b的分支兩兩組合！最後分支數量等於a分支數量乘以b分支數量。」

「很好。若是Any類比加法，那麼All類比的是乘法。下面這圖描述了開頭例子中的All方法的結合過程。

「這是個有向圖，每條邊表示一次追加條件的過程。每條從開始節點（上下文）到結尾的路徑，上面的節點組合起來就是一個替換。遍歷全部路徑，咱們就遍歷了全部替換。而遍歷的順序，就是解釋器輸出結果的順序。」

Anyi

接下來咱們還能夠來看看Anyi。

普通的Any使用的普通的樹結構遍歷順序：

而Anyi以交替的順序遍歷分支：

Alli相似採用交替的順序遍歷，這裏就再也不畫了（主要是很差畫，懶）。

再看目標（Goal）

上一篇主要從構造目標的角度出發，介紹了不一樣方式構造出來的目標。爲了實現NMiniKanren的解釋器，咱們須要更加深刻地瞭解在解釋器的實現中，Goal是什麼類型。

在前面的討論中，咱們知道，目標的含義是對上下文/一個替換按照某種方式追加一些條件，返回零個、一個或多個替換——Eq返回一個；Any和All可能返回多個；另外前面沒討論到的Fail會返回零個。

從這個描述不難看出，最方便表述目標類型的是一個單參數函數，其參數是一個替換，返回值是替換的枚舉，至關於C#中的Enumerable<替換>，也能夠說是一個替換的流（Stream）。

Goal: (替換) -> Stream<替換>

Goal(替換)這個函數調用的含義是把Goal包含的條件，追加到替換上，返回一系列（由於可能有分支，就會變成多個）的替換。

「爲何不直接用List呢？」小皮又發問了。

「由於不少狀況下，分支數量會不少，甚至是無窮多，而咱們只須要挨個取前面幾個結果就夠了。這種狀況下使用List會極大下降解釋器效率，甚至形成死循環。」

遞歸的狀況

「略。」

「啥？」小皮瞪了下眼。

「懶得畫，留着思考吧。」

替換求解

「生成替換後，剩下的就是求解了。

「替換求解的方法很簡單，就是應用一下小學時學過的代入消元法。來，看看這個怎麼解。」老明一邊說一邊寫下例題：

(1) y == x
(2) q == (x y)
(3) x == 1

畢竟是小學難度的題目，小皮看了一眼，立刻就有了解法：「x等於1是肯定的了，把(3)代入(1)後，y也等於1。把(1)和(3)都代入(2)，獲得q等於(1 1)。」

「解是求出來了，不過你以爲你這個步驟有通用性嗎？」老明虛着眼說，「計算機能自覺地使用你這個蛇皮順序嗎？」

「呃……」小皮陷入沉思。判斷代入順序的規則彷佛還挺麻煩的。或者簡單粗暴按照全部順序都代入一遍？

「其實沒想象中複雜，按順序代入一遍，再反過來代入一遍，就OK了。」

按順序代入

把(1)代入(2)(3)：

(1) y == x
(2) q == (x x)
(3) x == 1

把(2)代入(3)：

(1) y == x
(2) q == (x x)
(3) x == 1

在解釋器實現中，條件是一條一條追加上來的。能夠每次追加條件的時候，將已有的條件代入新條件，這樣就把這一步化解到生成替換的過程當中了。

加入條件(1) y == x:

(1) y == x

加入條件(2) q == (x y):

(1) y == x
(2) q == (x x)

加入條件(3) x == 1:

(1) y == x
(2) q == (x x)
(3) x == 1

按相反順序代入

把(3)代入(2)(1)：

(1) y == 1
(2) q == (1 1)
(3) x == 1

把(2)代入(1)：

(1) y == 1
(2) q == (1 1)
(3) x == 1

搞定！

這只是個簡單的例子。實際狀況還可能會出現無解、自由變量以及死循環等狀況。這裏就很少贅述了。

再議「非」運算

「如今能看出NMiniKanren爲何不支持‘非’運算了嗎？」

小皮認真想了一會，說：「豈止不支持‘非’，‘大於’和‘小於’這些也不行吧。按照代入消元法，NMiniKanren只支持相等條件。」。

「那若是要支持這些運算應該怎麼作呢？」

「要拓展條件的類型。除了相等條件，還要有不相等條件等。響應的求解算法也要有所變化。」

「沒錯。改動雖然不大，可是代碼看起來會混亂得多。因此以教學爲目的的話，就不支持這些了。」

小結

不知不覺時間已到了喜聞樂見的午飯時間，因而老明總結道：「雖然尚未落地成代碼，但運行原理算是弄清楚了。關鍵點就兩個:

1. 要在什麼數據結構上按照什麼順序遍歷替換。
2. 如何從替換中算出一個解，或者判斷其無解。

「第一點，咱們從代碼構造了一張圖。該圖的每條路徑對應一個替換，遍歷路徑的順序就是遍歷替換的順序。同時也明確了目標Goal的類型。

「第二點，咱們使用代入消元法，來回兩遍代入解出了全部未知量。」

「接下來能夠寫代碼實現NMiniKanren解釋器了吧。」理解了原理後，小皮的十條手指已經飢渴難耐，蚯蚓似的扭動着。

「不着急，下午還要先講一個編程小技巧，而後就能夠開搞了。」