圖文講解，一門教學級邏輯式編程語言，NMiniKanren，的運行原理。 ...
本系列前面的文章：
第二天，好為人師的老明繼續開講他的私人課堂。
“今天講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 == 1y == x => (x y) == (1 1)y == "b" => (x y) == (1 "b")
x == 2y == x => (x y) == (2 2)y == "b" => (x y) == (2 "b")
“嗯，其實你已經知道怎麼算出答案來了。只是對於其中的細節還不甚明瞭。我們接下來要做的事要理清楚這個計算過程，得到一個每一步都可以由電腦明確執行的演算法。
“這個演算法其實就是你所說這樣，找出所有可能的條件組合。每組條件組合可以求出一個解，也可能自相矛盾從而無解。由於NMiniKanren中的條件都是相等條件，所以一組條件組合可以看作一個替換（Substitution）。一個替換能產生一個解，或者無解。
“因此，只需解決下麵兩個問題：
- 要在什麼數據結構上按照什麼順序遍歷替換。
- 如何從替換中算出一個解，或者判斷其無解。”
遍歷分支
首先，我們要從代碼構造出一個數據結構（其實就是一張圖）。這個數據結構能夠按照一定的順序進行遍歷，並依次生成替換。
例子中的代碼使用到了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只支持相等條件。”。
“那如果要支持這些運算應該怎麼做呢？”
“要拓展條件的類型。除了相等條件，還要有不相等條件等。響應的求解演算法也要有所變化。”
“沒錯。改動雖然不大，但是代碼看起來會混亂得多。所以以教學為目的的話，就不支持這些了。”
小結
不知不覺時間已到了喜聞樂見的午餐時間，於是老明總結道：“雖然還沒有落地成代碼，但運行原理算是弄清楚了。關鍵點就兩個:
- 要在什麼數據結構上按照什麼順序遍歷替換。
- 如何從替換中算出一個解，或者判斷其無解。
“第一點，我們從代碼構造了一張圖。該圖的每條路徑對應一個替換，遍歷路徑的順序就是遍歷替換的順序。同時也明確了目標Goal的類型。
“第二點，我們使用代入消元法，來回兩遍代入解出了所有未知量。”
“接下來可以寫代碼實現NMiniKanren解釋器了吧。”理解了原理後，小皮的十條手指已經饑渴難耐，蚯蚓似的扭動著。
“不著急，下午還要先講一個編程小技巧，然後就可以開搞了。”
