本文是本系列的完結篇。本系列前面的文章： * [邏輯式程式語言極簡實現（使用C#） - 1. 邏輯式程式語言介紹](https://www.cnblogs.com/skabyy/p/13199800.html) * [邏輯式程式語言極簡實現（使用C#） - 2. 一道邏輯題：誰是凶手](https://www.cnblogs.com/skabyy/p/13199805.html) * [邏輯式程式語言極簡實現（使用C#） - 3. 執行原理](https://www.cnblogs.com/skabyy/p/13209724.html) 下午，吃飽飯的老明和小皮，各拿著一杯剛買的咖啡回到會議室，開始了邏輯式程式語言的最後一課。 老明喝了一口咖啡，說：“你看咖啡機，是不是咖啡的列表。” “啥？”小皮有點懵圈，“你說工廠的話還好理解，列表不太像。” “每次點一下按鈕，就相當於呼叫了一次next，出來一杯咖啡。而它本身並不包含咖啡，每一次都是現場磨豆衝出來的。這正是一個典型的惰性列表。” “有點道理，但是這跟邏輯式程式語言直譯器有什麼關係呢？” “這就是下面要說的流計算模式，它是實現分支遍歷的核心技巧。” 下面先講流計算模式，然後再講替換求解的實現與分支遍歷的實現。 ## 流（Stream）計算模式 老明在白板上寫下“Stream”，說：“Stream最常見的用途是用來表示數量未知或者無窮的列表。在程式碼中怎麼定義流呢？我們先來看看自然數，自然數是無窮的，那我們怎麼定義自然數列呢？” “這很顯然，不就是0、1、2、3、4、5等等吧。” 老明鄙夷地看著小皮，說：“如果我是你的數學老師，那我肯定要罰你站在牆角數完所有自然數……想想數學歸納法！” “哦哦，哎！數學這些烏漆嘛黑的知識總是喜歡偷偷溜走。自然數的定義簡單來說（~~嚴謹的不會~~），由兩部分組成： 1. （起點部分）0是自然數； 2. （遞迴部分）任意自然數加1也是自然數。 “這樣我們根據第1部分，得到起點0；再根據第2部分，一直加1，依次得到1、2、3、4、5等自然數。” “看來基礎還是不錯的。”老明微笑著點點頭，然後開始進入正文…… 從自然數的定義，我們可以得到啟發，**Stream的定義也是由兩部分組成**： 1. **起點**：第一個元素（非空流）； 2. **遞迴**：一個無參函式，呼叫它會返回這個Stream去掉第一個元素後剩下部分組成的剩餘Stream。 **第2部分之所以是個函式，是為了獲得惰性的效果，僅當需要時才計算剩餘的Stream**。 使用程式碼定義Stream如下： ```CSharp public delegate Stream DelayedStream(); // Stream的定義，我們只會用到替換的Stream，所以這裡就不做泛型了。 public class Stream { // 第一個元素，型別為Substitution（替換） public Substitution Curr { get; set; } // 獲取剩餘Stream的方法 public DelayedStream GetRest { get; set; } private static Stream MakeStream(Substitution curr, DelayedStream getRest) { return new Stream() { Curr = curr, GetRest = getRest }; } ... } ``` 其中`Substitution`是替換類，後面會講到這個類的實現。 還需要定義一個空Stream，除了表示空以外，還用來作為有限Stream的結尾。空Stream是一個特殊的單例。 > 正常來講，空Stream應該額外宣告一個型別。這裡偷了個懶。 ```CSharp private Stream() { } private static readonly Stream theEmptyStream = new Stream(); public bool IsEmpty() { return this == theEmptyStream; } public static Stream Empty() { return theEmptyStream; } ``` 特別的，還需要一個構造單元素的Stream的方法： ```CSharp public static Stream Unit(Substitution sub) { return MakeStream(sub, () => Empty()); } ``` 只有這些平凡的構造方法還看不出Stream的用處，接下來結合前面講過的NMiniKanren執行原理，探索如何使用Stream來實現替換的遍歷。 ### Append方法 回顧一下`Any`的執行原理，`Any`的每個引數會各自返回一個Stream。這些Stream代表了各個引數包含的可能性。`Any`操作把所有可能性放在一起，也就是把這些Stream拼在一起組成一個長長的Stream。  所以相應的，我們需要把兩個Stream `s1`和`s2`拼接成一個“長”Stream的Append方法。 如何構造這個“長”Stream呢？ 首先，如果`s1`是空Stream，那麼拼接後的Stream顯然就是`s2`。 否則，按照Stream定義，分兩個部分進行構造： 1. 第一個元素，顯然就是`s1`的第一個元素； 2. 剩餘Stream，就是`s1`的剩餘Stream，拼上`s2`，這裡是個遞迴定義。 按照上面分析的構造方法，我們就能輕鬆地寫下程式碼： ```CSharp public Stream Append(DelayedStream f) { if (IsEmpty()) return f(); return MakeStream(Curr, () => GetRest().Append(f)); } ``` 在這個實現中，`f`是尚未計算的`s2`。我們需要儘量推遲`s2`第一個元素的計算，因為推遲著推遲著可能就沒了不用算了。在很多場景中，這個可以節省不必要的計算，甚至避免死迴圈（“這都是血淚教訓。”老明捂臉）。 下面是一個`Any`與`Append`的例子：  ### Interleave方法 `Anyi`和`Any`的區別只有順序。`Anyi`使用交替的順序。 所以相應的，我們需要一個方法，這個方法把兩個Stream `s1`和`s2`中的元素交替地拼接組成一個“長”Stream。  首先，如果`s1`是空Stream，那麼“長”Stream顯然就是`s2`。 否則，分兩部分構造： 1. 第一個元素是`s1`的第一個元素； 2. 這裡和Append方法的區別是把`s1`和`s2`的位置調換了，剩餘Stream是`s2`交替拼上`s1`的剩餘Stream，同樣是個遞迴定義。 程式碼如下： ```CSharp public Stream Interleave(DelayedStream f) { if (IsEmpty()) return f(); return MakeStream(Curr, () => f().Interleave(GetRest)); } ``` 這裡使用惰性的`f`是非常必要的，因為我們不希望取剩餘Stream的時候呼叫`GetRest`。 ### Bind方法 這個方法比較複雜，是對應到`All`運算中兩兩組合引數裡的分支的過程。  不同於`Append`/`Interleave`作用在兩個Stream上，`Bind`方法作用在一個Stream和一個Goal上。 為什麼不是兩個Stream呢？ 前面已經分析過了，`k.All(g1, g2)`這個運算，是把`g2`蘊含的條件，追加到`g1`所包含的Stream中的每個替換裡。 同時，`g2`是個函式。追加這個動作本身由`g2`表達。 舉例來說，假設`st`是`g1`所包含的Stream中的一個替換。那麼把`g2`蘊含的條件追加到`st`上，其結果為`g2(st)`。 正是因為`Bind`方法中需要有追加條件這個動作，所以`Bind`方法的第二個引數只能是既包含了條件內容，也包含了追加方法的Goal型別。 用記號`s1`表示`g1`所包含的Stream，`Bind`方法的作用就是把`g2`蘊含的條件追加到`s1`中的每個替換裡。 首先，如果`s1`是個空Stream，那顯然`Bind`的結果是空Stream。 否則，結果是`s1`的第一個元素追加`g2`，再拼上`s1`的剩餘Stream `Bind` `g2`的結果。這仍是遞迴定義，不過是藉助的`Append`方法進行Stream構造。 程式碼如下： ```CSharp public Stream Bind(Goal g) { if (IsEmpty()) return Empty(); return g(Curr).Append(() => GetRest().Bind(g)); } ``` > 這個方法為什麼叫`Bind`，因為取名廢只好抄《The Reasoned Schemer》裡的命名…… 下面是一個`All`與`Bind`的例子：  ### Bindi方法 對應`Alli`，交替版的`Bind`方法。程式碼實現不再多說，直接把`Bind`實現中的`Append`換成`Interleave`即可： ```CSharp public Stream Bindi(Goal g) { if (IsEmpty()) return Empty(); return g(Curr).Interleave(() => GetRest().Bindi(g)); } ``` > 更多Stream的玩法，參見《計算機程式的構造和解釋》（簡稱《SICP》）第三章。 ## 替換求解的實現 構造目標時會用到替換裡的方法，所以和上一篇順序相反，先講替換求解。 ### 替換 替換的定義為： ```CSharp public class Substitution { private readonly Substitution parent; public FreshVariable Var { get; } public object Val { get; } private Substitution(Substitution p, FreshVariable var, object val) { parent = p; Var = var; Val = val; } private static readonly Substitution theEmptySubstitution = new Substitution(null, null, null); public static Substitution Empty() { return theEmptySubstitution; } public bool IsEmpty() { return this == theEmptySubstitution; } public Substitution Extend(FreshVariable var, object val) { return new Substitution(this, var, val); } public bool Find(FreshVariable var, out object val) { if (IsEmpty()) { val = null; return false; } if (Var == var) { val = Val; return true; } return parent.Find(var, out val); } ... } ``` 這是個單鏈表的結構。我們需要能在替換中追根溯源地查詢未知量的值的方法（也就是將條件代入到未知量）： ```CSharp public object Walk(object v) { if (v is KPair p) { return new KPair(Walk(p.Lhs), Walk(p.Rhs)); } if (v is FreshVariable var && Find(var, out var val)) { return Walk(val); } return v; } ``` 例如在替換`(x=1, q=(x y), y=x)`中，`Walk(q)`返回`(1 1)`。 注意替換結構裡面，條件都是`未知量 = 值`的形式。但是在NMiniKanren程式碼中並非所有條件都是這種形式。所以在追加條件時，需要先將條件轉化為`未知量 = 值`的形式。 追加條件時，不是簡單的使用`Extend`方法，而是用`Unify`方法。`Unify`方法結合了`Extend`和代入消元法。它先將已有條件代入到新條件中，然後再把代入後的新條件轉化為`未知量 = 值`的形式： ```CSharp public Substitution Unify(object v1, object v2) { v1 = Walk(v1); // 使用已知條件代入到v1 v2 = Walk(v2); // 使用已知條件代入到v2 if (v1 is KPair p1 && v2 is KPair p2) { return Unify(p1.Lhs, p2.Lhs)?.Unify(p1.Rhs, p2.Rhs); } if (v1 is FreshVariable var1) { return Extend(var1, v2); } if (v2 is FreshVariable var2) { return Extend(var2, v1); } // 兩邊都是值。值相等的話替換不變；值不相等返回null表示矛盾。 if (v1 == null) { if (v2 == null) return this; } else { if (v1.Equals(v2)) return this; } return null; } ``` `Unify`方法實現了代入消元的第一遍代入（詳情見[上一篇](https://www.cnblogs.com/skabyy/p/13209724.html)）。`Unify`的全拼是unification，中文叫合一。 ### 求解 由於NMiniKanren的輸出只有未知量`q`，所以第二遍代入的過程只需要查詢`q`的值即可： ```CSharp Walk(q) ``` ## 構造目標的實現 通過Stream的分析，我們知道，只要構造了目標，自然就實現了分支的遍歷。 ### Success與Fail 任何替換追加`Success`，相當於沒追加，所以`k.Success`直接返回一個只包含上下文的Stream： ```CSharp public Goal Succeed = sub => Stream.Unit(sub); ``` 任何替換追加`Fail`，那它這輩子就完了，`k.Fail`直接返回空Stream ```CSharp public Goal Fail => sub => Stream.Empty(); ``` ### Eq `k.Eq(v1, v2)`向上下文追加`v1 == v2`條件。 首先，使用`Unify`方法將`v1 == v2`條件擴充套件到上下文代表的替換。 若擴充套件後的替換出現矛盾，表示無解，返回空Stream。 否則返回只包含擴充套件後的替換的Stream。 程式碼如下： ```CSharp public Goal Eq(object v1, object v2) { return sub => { var u = sub.Unify(v1, v2); if (u == null) { return Stream.Empty(); } return Stream.Unit(u); }; } ``` ### Any/Anyi 首先，利用`Stream.Append`實現二目運算版本的`Or`： ```CSharp public Goal Or(Goal g1, Goal g2) { return sub => g1(sub).Append(() => g2(sub)); } ``` 然後擴充套件到多引數： ```CSharp public Goal Any(params Goal[] gs) { if (gs.Length == 0) return Fail; if (gs.Length == 1) return gs[0]; return Or(gs[0], Any(gs.Skip(1).ToArray())); } ``` 同理實現`Ori`和`Anyi`： ```CSharp public Goal Ori(Goal g1, Goal g2) { return sub => g1(sub).Interleave(() => g2(sub)); } public Goal Anyi(params Goal[] gs) { if (gs.Length == 0) return Fail; if (gs.Length == 1) return gs[0]; return Ori(gs[0], Anyi(gs.Skip(1).ToArray())); } ``` ### All/Alli 利用`Stream.Bind`實現二目版本的`And`： ```CSharp public Goal And(Goal g1, Goal g2) { return sub => g1(sub).Bind(g2); } ``` 然後擴充套件到多引數： ```CSharp public Goal All(params Goal[] gs) { if (gs.Length == 0) return Succeed; if (gs.Length == 1) return gs[0]; return And(gs[0], All(gs.Skip(1).ToArray())); } ``` 同理實現`Andi`和`Alli`： ```CSharp public Goal Andi(Goal g1, Goal g2) { return sub => g1(sub).Bindi(g2); } public Goal Alli(params Goal[] gs) { if (gs.Length == 0) return Succeed; if (gs.Length == 1) return gs[0]; return Andi(gs[0], All(gs.Skip(1).ToArray())); } ``` ## 串起來執行，以及一些細枝末節 ```CSharp public static IList