邏輯式編程語言極簡實作（使用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解釋器了吧，”理解了原理后，小皮的十條手指已經饑渴難耐，蚯蚓似的扭動著，

“不著急，下午還要先講一個編程小技巧，然后就可以開搞了，”

標籤：C#

上一篇：串口通訊學習

下一篇：C#6.0到C#8.0的新特性