神奇，實作一門邏輯式語音竟然隻需兩頁代碼~
本文是本系列的完結篇。本系列前面的文章：
邏輯式程式設計語言極簡實作（使用C#） - 1. 邏輯式程式設計語言介紹
邏輯式程式設計語言極簡實作（使用C#） - 2. 一道邏輯題：誰是兇手
邏輯式程式設計語言極簡實作（使用C#） - 3. 運作原理
下午，吃飽飯的老明和小皮，各拿着一杯剛買的咖啡回到會議室，開始了邏輯式程式設計語言的最後一課。
老明喝了一口咖啡，說：“你看咖啡機，是不是咖啡的清單。”
“啥？”小皮有點懵圈，“你說工廠的話還好了解，清單不太像。”
“每次點一下按鈕，就相當于調用了一次next，出來一杯咖啡。而它本身并不包含咖啡，每一次都是現場磨豆沖出來的。這正是一個典型的惰性清單。”
“有點道理，但是這跟邏輯式程式設計語言解釋器有什麼關系呢？”
“這就是下面要說的流計算模式，它是實作分支周遊的核心技巧。”
下面先講流計算模式，然後再講替換求解的實作與分支周遊的實作。
老明在白闆上寫下“Stream”，說：“Stream最常見的用途是用來表示數量未知或者無窮的清單。在代碼中怎麼定義流呢？我們先來看看自然數，自然數是無窮的，那我們怎麼定義自然數列呢？”
“這很顯然，不就是0、1、2、3、4、5等等吧。”
老明鄙夷地看着小皮，說：“如果我是你的數學老師，那我肯定要罰你站在牆角數完所有自然數……想想數學歸納法！”
“哦哦，哎！數學這些烏漆嘛黑的知識總是喜歡偷偷溜走。自然數的定義簡單來說（嚴謹的不會），由兩部分組成：
（起點部分）0是自然數；
（遞歸部分）任意自然數加1也是自然數。
“這樣我們根據第1部分，得到起點0；再根據第2部分，一直加1，依次得到1、2、3、4、5等自然數。”
“看來基礎還是不錯的。”老明微笑着點點頭，然後開始進入正文……
從自然數的定義，我們可以得到啟發，Stream的定義也是由兩部分組成：
起點：第一個元素（非空流）；
遞歸：一個無參函數，調用它會傳回這個Stream去掉第一個元素後剩下部分組成的剩餘Stream。
第2部分之是以是個函數，是為了獲得惰性的效果，僅當需要時才計算剩餘的Stream。
使用代碼定義Stream如下：
其中<code>Substitution</code>是替換類，後面會講到這個類的實作。
還需要定義一個空Stream，除了表示空以外，還用來作為有限Stream的結尾。空Stream是一個特殊的單例。
正常來講，空Stream應該額外聲明一個類型。這裡偷了個懶。
特别的，還需要一個構造單元素的Stream的方法：
隻有這些平凡的構造方法還看不出Stream的用處，接下來結合前面講過的NMiniKanren運作原理，探索如何使用Stream來實作替換的周遊。
回顧一下<code>Any</code>的運作原理，<code>Any</code>的每個參數會各自傳回一個Stream。這些Stream代表了各個參數包含的可能性。<code>Any</code>操作把所有可能性放在一起，也就是把這些Stream拼在一起組成一個長長的Stream。
是以相應的，我們需要把兩個Stream <code>s1</code>和<code>s2</code>拼接成一個“長”Stream的Append方法。
如何構造這個“長”Stream呢？
首先，如果<code>s1</code>是空Stream，那麼拼接後的Stream顯然就是<code>s2</code>。
否則，按照Stream定義，分兩個部分進行構造：
第一個元素，顯然就是<code>s1</code>的第一個元素；
剩餘Stream，就是<code>s1</code>的剩餘Stream，拼上<code>s2</code>，這裡是個遞歸定義。
按照上面分析的構造方法，我們就能輕松地寫下代碼：
在這個實作中，<code>f</code>是尚未計算的<code>s2</code>。我們需要盡量推遲<code>s2</code>第一個元素的計算，因為推遲着推遲着可能就沒了不用算了。在很多場景中，這個可以節省不必要的計算，甚至避免死循環（“這都是血淚教訓。”老明捂臉）。
下面是一個<code>Any</code>與<code>Append</code>的例子：
<code>Anyi</code>和<code>Any</code>的差別隻有順序。<code>Anyi</code>使用交替的順序。
是以相應的，我們需要一個方法，這個方法把兩個Stream <code>s1</code>和<code>s2</code>中的元素交替地拼接組成一個“長”Stream。
首先，如果<code>s1</code>是空Stream，那麼“長”Stream顯然就是<code>s2</code>。
否則，分兩部分構造：
第一個元素是<code>s1</code>的第一個元素；
這裡和Append方法的差別是把<code>s1</code>和<code>s2</code>的位置調換了，剩餘Stream是<code>s2</code>交替拼上<code>s1</code>的剩餘Stream，同樣是個遞歸定義。
代碼如下：
這裡使用惰性的<code>f</code>是非常必要的，因為我們不希望取剩餘Stream的時候調用<code>GetRest</code>。
這個方法比較複雜，是對應到<code>All</code>運算中兩兩組合參數裡的分支的過程。
不同于<code>Append</code>/<code>Interleave</code>作用在兩個Stream上，<code>Bind</code>方法作用在一個Stream和一個Goal上。
為什麼不是兩個Stream呢？
前面已經分析過了，<code>k.All(g1, g2)</code>這個運算，是把<code>g2</code>蘊含的條件，追加到<code>g1</code>所包含的Stream中的每個替換裡。
同時，<code>g2</code>是個函數。追加這個動作本身由<code>g2</code>表達。
舉例來說，假設<code>st</code>是<code>g1</code>所包含的Stream中的一個替換。那麼把<code>g2</code>蘊含的條件追加到<code>st</code>上，其結果為<code>g2(st)</code>。
正是因為<code>Bind</code>方法中需要有追加條件這個動作，是以<code>Bind</code>方法的第二個參數隻能是既包含了條件内容，也包含了追加方法的Goal類型。
用記号<code>s1</code>表示<code>g1</code>所包含的Stream，<code>Bind</code>方法的作用就是把<code>g2</code>蘊含的條件追加到<code>s1</code>中的每個替換裡。
首先，如果<code>s1</code>是個空Stream，那顯然<code>Bind</code>的結果是空Stream。
否則，結果是<code>s1</code>的第一個元素追加<code>g2</code>，再拼上<code>s1</code>的剩餘Stream <code>Bind</code> <code>g2</code>的結果。這仍是遞歸定義，不過是借助的<code>Append</code>方法進行Stream構造。
這個方法為什麼叫<code>Bind</code>，因為取名廢隻好抄《The Reasoned Schemer》裡的命名……
下面是一個<code>All</code>與<code>Bind</code>的例子：
對應<code>Alli</code>，交替版的<code>Bind</code>方法。代碼實作不再多說，直接把<code>Bind</code>實作中的<code>Append</code>換成<code>Interleave</code>即可：
更多Stream的玩法，參見《計算機程式的構造和解釋》（簡稱《SICP》）第三章。
構造目标時會用到替換裡的方法，是以和上一篇順序相反，先講替換求解。
替換的定義為：
這是個單連結清單的結構。我們需要能在替換中追根溯源地查找未知量的值的方法（也就是将條件代入到未知量）：
例如在替換<code>(x=1, q=(x y), y=x)</code>中，<code>Walk(q)</code>傳回<code>(1 1)</code>。
注意替換結構裡面，條件都是<code>未知量 = 值</code>的形式。但是在NMiniKanren代碼中并非所有條件都是這種形式。是以在追加條件時，需要先将條件轉化為<code>未知量 = 值</code>的形式。
追加條件時，不是簡單的使用<code>Extend</code>方法，而是用<code>Unify</code>方法。<code>Unify</code>方法結合了<code>Extend</code>和代入消元法。它先将已有條件代入到新條件中，然後再把代入後的新條件轉化為<code>未知量 = 值</code>的形式：
<code>Unify</code>方法實作了代入消元的第一遍代入（詳情見上一篇）。<code>Unify</code>的全拼是unification，中文叫合一。
由于NMiniKanren的輸出隻有未知量<code>q</code>，是以第二遍代入的過程隻需要查找<code>q</code>的值即可：
通過Stream的分析，我們知道，隻要構造了目标，自然就實作了分支的周遊。
任何替換追加<code>Success</code>，相當于沒追加，是以<code>k.Success</code>直接傳回一個隻包含上下文的Stream：
任何替換追加<code>Fail</code>，那它這輩子就完了，<code>k.Fail</code>直接傳回空Stream
<code>k.Eq(v1, v2)</code>向上下文追加<code>v1 == v2</code>條件。
首先，使用<code>Unify</code>方法将<code>v1 == v2</code>條件擴充到上下文代表的替換。
若擴充後的替換出現沖突，表示無解，傳回空Stream。
否則傳回隻包含擴充後的替換的Stream。
首先，利用<code>Stream.Append</code>實作二目運算版本的<code>Or</code>：
然後擴充到多參數：
同理實作<code>Ori</code>和<code>Anyi</code>：
利用<code>Stream.Bind</code>實作二目版本的<code>And</code>：
同理實作<code>Andi</code>和<code>Alli</code>：
其中，<code>MapAndTake</code>方法取Stream的前n個（或所有）值，并map每一個值。
<code>Renumber</code>将自由變量替換成<code>_0</code>、<code>_1</code>……這類符号。
NMiniKanren的完整代碼在這裡：https://github.com/sKabYY/NMiniKanren
總結一下NMiniKanren的原理：
NMiniKanren代碼描述的是一個Goal。Goal是一個替換到Stream的函數。
從NMiniKanren代碼可以建構一張描述了條件關系的圖。每條路徑對應一個替換，使用流計算模式可以很巧妙地實作對所有路徑的周遊。
使用代入消元法求解未知量。
另外NMiniKanren畢竟隻是一門教學級的語言，實用上肯定一塌糊塗，說難聽點也就是個玩具。我們學習的重點不在于NMiniKanren，而在于實作NMiniKanren的過程中所用到的技術和思想。掌握了這些方法後，可以根據自己的需要進行優化或擴充，或者将這些方法應用到其他問題上。
“神奇！”小皮瞪着眼睛摸摸腦袋，以前覺得宛若天書般的邏輯式程式設計語言就這麼學完了，還包括了解釋器的實作。
“認真學習了一天半的效果還是不錯了。嘿嘿。”老明欣慰地拍了拍小皮的肩膀，微微笑道，“世上無難事，隻怕有心人。恰好今天周五了，周末就來公司把這兩天落下的工作補完吧。”
小皮：“？？？”
PS：最後，用《The Reasoned Schemer》裡的兩頁實作鎮樓。俗話說得好，C#隻是恰飯，真正的快樂還得看Scheme/Lisp。