(給DotNet加星标，提升.Net技能)
轉自：古霜卡比 cnblogs.com/skabyy/p/13232933.html
本文是本系列的完結篇。本系列前面的文章：
《邏輯式程式設計語言極簡實作(使用C#)：邏輯式程式設計語言介紹》
《邏輯式程式設計語言極簡實作(使用C#)：運作原理》
下午，吃飽飯的老明和小皮，各拿着一杯剛買的咖啡回到會議室，開始了邏輯式程式設計語言的最後一課。
老明喝了一口咖啡，說：你看咖啡機，是不是咖啡的清單。
啥？小皮有點懵圈，你說工廠的話還好了解，清單不太像。
每次點一下按鈕，就相當于調用了一次next，出來一杯咖啡。而它本身并不包含咖啡，每一次都是現場磨豆沖出來的。這正是一個典型的惰性清單。
有點道理，但是這跟邏輯式程式設計語言解釋器有什麼關系呢？
這就是下面要說的流計算模式，它是實作分支周遊的核心技巧。
下面先講流計算模式，然後再講替換求解的實作與分支周遊的實作。
流(Stream)計算模式
老明在白闆上寫下Stream，說：Stream最常見的用途是用來表示數量未知或者無窮的清單。在代碼中怎麼定義流呢？我們先來看看自然數，自然數是無窮的，那我們怎麼定義自然數列呢？
這很顯然，不就是0、1、2、3、4、5等等吧。
老明鄙夷地看着小皮，說：如果我是你的數學老師，那我肯定要罰你站在牆角數完所有自然數……想想數學歸納法！
哦哦，哎！數學這些烏漆嘛黑的知識總是喜歡偷偷溜走。自然數的定義簡單來說(嚴謹的不會)，由兩部分組成：
- (起點部分)0是自然數；
- (遞歸部分)任意自然數加1也是自然數。
這樣我們根據第1部分，得到起點0；再根據第2部分，一直加1，依次得到1、2、3、4、5等自然數。
看來基礎還是不錯的。老明微笑着點點頭，然後開始進入正文……
從自然數的定義，我們可以得到啟發，Stream的定義也是由兩部分組成：
1、起點：第一個元素(非空流)；
2、遞歸：一個無參函數，調用它會傳回這個Stream去掉第一個元素後剩下部分組成的剩餘Stream。
第2部分之是以是個函數，是為了獲得惰性的效果，僅當需要時才計算剩餘的Stream。
使用代碼定義Stream如下：
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應該額外聲明一個類型。這裡偷了個懶。
private Stream() { }
private static readonly Stream theEmptyStream = new Stream();
public bool IsEmpty(){
return this == theEmptyStream;
}
public static Stream Empty(){
return theEmptyStream;
}
特别的，還需要一個構造單元素的Stream的方法：
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，這裡是個遞歸定義。
按照上面分析的構造方法，我們就能輕松地寫下代碼：
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，同樣是個遞歸定義。
代碼如下：
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構造。
代碼如下：
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即可：
public Stream Bindi(Goal g)
{
if (IsEmpty()) return Empty();
return g(Curr).Interleave(() => GetRest().Bindi(g));
}
更多Stream的玩法，參見《計算機程式的構造和解釋》(簡稱《SICP》)第三章。
替換求解的實作
構造目标時會用到替換裡的方法，是以和上一篇順序相反，先講替換求解。
替換
替換的定義為：
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);
}
...
}
這是個單連結清單的結構。我們需要能在替換中追根溯源地查找未知量的值的方法(也就是将條件代入到未知量)：
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和代入消元法。它先将已有條件代入到新條件中，然後再把代入後的新條件轉化為未知量 = 值的形式：
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方法實作了代入消元的第一遍代入(詳情見上一篇)。Unify的全拼是unification，中文叫合一。
求解
由于NMiniKanren的輸出隻有未知量q，是以第二遍代入的過程隻需要查找q的值即可：
Walk(q)
構造目标的實作
通過Stream的分析，我們知道，隻要構造了目标，自然就實作了分支的周遊。
Success與Fail
任何替換追加Success，相當于沒追加，是以k.Success直接傳回一個隻包含上下文的Stream：
public Goal Succeed = sub => Stream.Unit(sub);
任何替換追加Fail，那它這輩子就完了，k.Fail直接傳回空Stream
public Goal Fail => sub => Stream.Empty();
Eq
k.Eq(v1, v2)向上下文追加v1 == v2條件。
首先，使用Unify方法将v1 == v2條件擴充到上下文代表的替換。
若擴充後的替換出現沖突，表示無解，傳回空Stream。
否則傳回隻包含擴充後的替換的Stream。
代碼如下：
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：
public Goal Or(Goal g1, Goal g2)
{
return sub => g1(sub).Append(() => g2(sub));
}
然後擴充到多參數：
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：
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：
public Goal And(Goal g1, Goal g2)
{
return sub => g1(sub).Bind(g2);
}
然後擴充到多參數：
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：
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()));
}
串起來運作，以及一些細枝末節
public static IList<object> Run(int? n, Func body){
var k = new KRunner();
// 定義待求解的未知量q
var q = k.Fresh();
// 執行body，得到最終目标g
var g = body(k, q);
// 初始上下文是一個空替換，應用到g，得到包含可行替換的Stream s
var s = g(Substitution.Empty());
// 從s中取出前n個(n==null則取所有)替換，查找各個替換下q的解，并給自由變量換個好看的符号。
return s.MapAndTake(n, sub => Renumber(sub.Walk(q)));
}
其中，MapAndTake方法取Stream的前n個(或所有)值，并map每一個值。
Renumber将自由變量替換成_0、_1……這類符号。
NMiniKanren的完整代碼在這裡：https://github.com/sKabYY/NMiniKanren
結尾
總結一下NMiniKanren的原理：
- NMiniKanren代碼描述的是一個Goal。Goal是一個替換到Stream的函數。
- 從NMiniKanren代碼可以建構一張描述了條件關系的圖。每條路徑對應一個替換，使用流計算模式可以很巧妙地實作對所有路徑的周遊。
- 使用代入消元法求解未知量。
另外NMiniKanren畢竟隻是一門教學級的語言，實用上肯定一塌糊塗，說難聽點也就是個玩具。我們學習的重點不在于NMiniKanren，而在于實作NMiniKanren的過程中所用到的技術和思想。掌握了這些方法後，可以根據自己的需要進行優化或擴充，或者将這些方法應用到其他問題上。
神奇！小皮瞪着眼睛摸摸腦袋，以前覺得宛若天書般的邏輯式程式設計語言就這麼學完了，還包括了解釋器的實作。
認真學習了一天半的效果還是不錯了。嘿嘿。老明欣慰地拍了拍小皮的肩膀，微微笑道，世上無難事，隻怕有心人。恰好今天周五了，周末就來公司把這兩天落下的工作補完吧。
小皮：？？？
PS：最後，用《The Reasoned Schemer》裡的兩頁實作鎮樓。俗話說得好，C#隻是恰飯，真正的快樂還得看Scheme/Lisp。
- EOF -
推薦閱讀 點選标題可跳轉
Entity Framework Core 開發實踐問題及規範
[開源].NET 使用 ORM 通路 神舟通用資料庫
了解C#中的ValueTask
看完本文有收獲？請轉發分享給更多人
關注「DotNet」加星标，提升.Net技能
好文章，我在看❤️