邏輯式編程語言極簡實現（使用C#） - 4. 代碼實現（完結）

時間 2020-07-07

標籤邏輯編程語言實現使用 c# 代碼完結欄目 C# 简体版

原文原文鏈接

本文是本系列的完結篇。本系列前面的文章：html

下午，吃飽飯的老明和小皮，各拿着一杯剛買的咖啡回到會議室，開始了邏輯式編程語言的最後一課。git

老明喝了一口咖啡，說：「你看咖啡機，是否是咖啡的列表。」github

「啥？」小皮有點懵圈，「你說工廠的話還好理解，列表不太像。」編程

「每次點一下按鈕，就至關於調用了一次next，出來一杯咖啡。而它自己並不包含咖啡，每一次都是現場磨豆衝出來的。這正是一個典型的惰性列表。」app

「有點道理，可是這跟邏輯式編程語言解釋器有什麼關係呢？」編程語言

「這就是下面要說的流計算模式，它是實現分支遍歷的核心技巧。」函數

下面先講流計算模式，而後再講替換求解的實現與分支遍歷的實現。學習

流（Stream）計算模式

老明在白板上寫下「Stream」，說：「Stream最多見的用途是用來表示數量未知或者無窮的列表。在代碼中怎麼定義流呢？咱們先來看看天然數，天然數是無窮的，那咱們怎麼定義天然數列呢？」優化

「這很顯然，不就是0、一、二、三、四、5等等吧。」this

老明鄙夷地看着小皮，說：「若是我是你的數學老師，那我確定要罰你站在牆角數完全部天然數……想一想數學概括法！」

「哦哦，哎！數學這些烏漆嘛黑的知識老是喜歡偷偷溜走。天然數的定義簡單來講（~~嚴謹的不會~~），由兩部分組成：

（起點部分）0是天然數；
（遞歸部分）任意天然數加1也是天然數。

「這樣咱們根據第1部分，獲得起點0；再根據第2部分，一直加1，依次獲得一、二、三、四、5等天然數。」

「看來基礎仍是不錯的。」老明微笑着點點頭，而後開始進入正文……

從天然數的定義，咱們能夠獲得啓發，Stream的定義也是由兩部分組成：

起點：第一個元素（非空流）；
遞歸：一個無參函數，調用它會返回這個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定義，分兩個部分進行構造：

第一個元素，顯然就是s1的第一個元素；
剩餘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。

不然，分兩部分構造：

第一個元素是s1的第一個元素；
這裏和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<KRunner, FreshVariable, Goal> 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