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

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

2020 年 7 月 2 日
筆記
miniKanren, Prolog, The Reasoned Schemer, 程式語言, 邏輯式編程

本系列前面的文章：

第二天，好為人師的老明繼續開講他的私人課堂。

「今天講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）。一個替換能產生一個解，或者無解。

「因此，只需解決下面兩個問題：

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

遍歷分支

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

例子中的程式碼使用到了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解釋器了吧。」理解了原理後，小皮的十條手指已經饑渴難耐，蚯蚓似的扭動著。

「不著急，下午還要先講一個編程小技巧，然後就可以開搞了。」

Tags: miniKanren Prolog The Reasoned Schemer 程式語言邏輯式編程