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

来源:https://www.cnblogs.com/skabyy/archive/2020/07/06/13232933.html
-Advertisement-
Play Games

本文是本系列的完結篇。本系列前面的文章： 邏輯式編程語言極簡實現（使用C#） - 1. 邏輯式編程語言介紹 邏輯式編程語言極簡實現（使用C#） - 2. 一道邏輯題：誰是凶手 邏輯式編程語言極簡實現（使用C#） - 3. 運行原理 下午，吃飽飯的老明和小皮，各拿著一杯剛買的咖啡回到會議室，開始了邏輯 ...


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

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

老明喝了一口咖啡，說：“你看咖啡機，是不是咖啡的列表。”

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

“每次點一下按鈕，就相當於調用了一次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如下：

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<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

結尾

總結一下NMiniKanren的原理：

  1. NMiniKanren代碼描述的是一個Goal。Goal是一個替換到Stream的函數。
  2. 從NMiniKanren代碼可以構建一張描述了條件關係的圖。每條路徑對應一個替換，使用流計算模式可以很巧妙地實現對所有路徑的遍歷。
  3. 使用代入消元法求解未知量。

另外NMiniKanren畢竟只是一門教學級的語言，實用上肯定一塌糊塗，說難聽點也就是個玩具。我們學習的重點不在於NMiniKanren，而在於實現NMiniKanren的過程中所用到的技術和思想。掌握了這些方法後，可以根據自己的需要進行優化或擴展，或者將這些方法應用到其他問題上。

“神奇！”小皮瞪著眼睛摸摸腦袋，以前覺得宛若天書般的邏輯式編程語言就這麼學完了，還包括瞭解釋器的實現。

“認真學習了一天半的效果還是不錯了。嘿嘿。”老明欣慰地拍了拍小皮的肩膀，微微笑道，“世上無難事，只怕有心人。恰好今天周五了，周末就來公司把這兩天落下的工作補完吧。”

小皮：“？？？”

PS：最後，用《The Reasoned Schemer》里的兩頁實現鎮樓。俗話說得好，C#只是恰飯，真正的快樂還得看Scheme/Lisp。


您的分享是我們最大的動力!

-Advertisement-
Play Games
更多相關文章
  • golang每日新聞之對我有益的文章總集
    一直想深入go語言，下定決心今年要狠抓go語言 | 文章名稱 | 文章鏈接 | | | | | Golang網路編程 | https://www.cnblogs.com/ZhuChangwu/p/13198872.html | | | | | | | ...
  • Java啟動新線程的幾種方式（Runnable、Callable、CompletableFuture）
    一、實現Runnable介面 public class RunnableDemo implements Runnable { public void run() { try { Thread.sleep(100); } catch (InterruptedException e) { e.print ...
  • C# 基於內容電影推薦項目（一）
    從今天起，我將製作一個電影推薦項目，在此寫下博客，記錄每天的成果。 其實，從我發佈 C# 爬取貓眼電影數據 這篇博客後， 我就已經開始製作電影推薦項目了，今天寫下這篇博客，也是因為項目進度已經完成50%了，我就想在這一階段停一下，回顧之前學到的知識。 一、主要為手機端 考慮到項目要有實用性，我選擇了 ...
  • csharp: Emgu.CV.OCR and Tesseract.OCR Optical Character Recognition
    using System; using System.Collections.Generic; using System.ComponentModel; using System.Data; using System.Drawing; using System.Linq; using System. ...
  • .Net Core微服務入門全紀錄（七）——IdentityServer4-授權認證
    前言 上一篇【.Net Core微服務入門全紀錄（六）——EventBus-事件匯流排】中使用CAP完成了一個簡單的Eventbus，實現了服務之間的解耦和非同步調用，並且做到數據的最終一致性。這一篇將使用IdentityServer4來搭建一個鑒權中心，來完成授權認證相關的功能。 IdentitySe ...
  • 簡述 private、 protected、 public、 internal 修飾符的訪問許可權。
    private:私有成員,在類的內部才可以訪問。 protected:保護成員，該類內部和繼承類中可以訪問。 public:公共成員，完全公開，沒有訪問限制。 internal:當前程式集內可以訪問。 ...
  • .NET中的線程本地存儲(TLS)與AsyncLocal（一）
    一、TLS 線程本地存儲（Thread Local Storage），字面意思就是專屬某個線程的存儲空間。變數大體上分為全局變數和局部變數，一個進程中的所有線程共用地址空間，這個地址空間被劃分為幾個固有的區域，比如堆棧區，全局變數區等，全局變數存儲在全局變數區，虛擬地址固定；局部變數存儲在堆棧區，虛... ...
  • 微服務 - 服務之間的通信gRPC
    微服務之間的通信之gRPC 介紹 gRPC是一種與語言無關的高性能遠程過程調用 (RPC) 框架，gRPC是Google發佈的基於HTTP 2.0傳輸層協議承載的高性能開源軟體框架，提供了支持多種編程語言的、對網路設備進行配置和納管的方法。由於是開源框架，通信的雙方可以進行二次開發，所以客戶端和服務 ...
一周排行
    -Advertisement-
    Play Games
  • C#自增運算符詳解：++i與i++的區別及應用場景
    概述：在C#中，++i和i++都是自增運算符，其中++i先增加值再返回，而i++先返回值再增加。應用場景根據需求選擇，首碼適合先增後用，尾碼適合先用後增。詳細示例提供清晰的代碼演示這兩者的操作時機和實際應用。 在C#中，++i 和 i++ 都是自增運算符，但它們在操作上有細微的差異，主要體現在操作的 ...
  • Taurus.MVC 性能壓力測試（ap 壓測 和 linux 下wrk 壓測）：.NET 版本
    上次發佈了：Taurus.MVC 性能壓力測試（ap 壓測 和 linux 下wrk 壓測）：.NET Core 版本，今天計劃準備壓測一下 .NET 版本，來測試並記錄一下 Taurus.MVC 框架在 .NET 版本的性能，以便後續持續優化改進。 為了方便對比，本文章的電腦環境和測試思路，儘量和... ...
  • 一文讀懂.NET WebAPI中FromRoute、FromQuery、FromBody的關鍵角色與用法
    .NET WebAPI作為一種構建RESTful服務的強大工具，為開發者提供了便捷的方式來定義、處理HTTP請求並返迴響應。在設計API介面時，正確地接收和解析客戶端發送的數據至關重要。.NET WebAPI提供了一系列特性，如[FromRoute]、[FromQuery]和[FromBody]，用 ...
  • WPF/C#實現圖像濾鏡優化方案：打造炫目視覺體驗！
    原因：我之所以想做這個項目，是因為在之前查找關於C#/WPF相關資料時，我發現講解圖像濾鏡的資源非常稀缺。此外，我註意到許多現有的開源庫主要基於CPU進行圖像渲染。這種方式在處理大量圖像時，會導致CPU的渲染負擔過重。因此，我將在下文中介紹如何通過GPU渲染來有效實現圖像的各種濾鏡效果。 生成的效果 ...
  • Bogus 實戰：使用 Bogus 和 EFCore 生成模擬數據和種子數據【完整教程】
    引言 上一章我們介紹了在xUnit單元測試中用xUnit.DependencyInject來使用依賴註入，上一章我們的Sample.Repository倉儲層有一個批量註入的介面沒有做單元測試，今天用這個示例來演示一下如何用Bogus創建模擬數據 ，和 EFCore 的種子數據生成 Bogus 的優 ...
  • WPF隨筆收錄-實時繪製心率曲線
    一、前言 在自己的項目中，涉及到實時心率曲線的繪製，項目上的曲線繪製，一般很難找到能直接用的第三方庫，而且有些還是定製化的功能，所以還是自己繪製比較方便。很多人一聽到自己畫就害怕，感覺很難，今天就分享一個完整的實時心率數據繪製心率曲線圖的例子；之前的博客也分享給DrawingVisual繪製曲線的方 ...
  • wpf程式修改啟動入口註意事項
    如果你在自定義的 Main 方法中直接使用 App 類並啟動應用程式，但發現 App.xaml 中定義的資源沒有被正確載入，那麼問題可能在於如何正確配置 App.xaml 與你的 App 類的交互。 確保 App.xaml 文件中的 x:Class 屬性正確指向你的 App 類。這樣，當你創建 Ap ...
  • 記一次 .NET某爐膛鍋爐檢測系統 崩潰分析
    一：背景 1. 講故事 上個月有個朋友在微信上找到我，說他們的軟體在客戶那邊隔幾天就要崩潰一次，一直都沒有找到原因，讓我幫忙看下怎麼回事，確實工控類的軟體環境複雜難搞，朋友手上有一個崩潰的dump，剛好丟給我來分析一下。 二：WinDbg分析 1. 程式為什麼會崩潰 windbg 有一個厲害之處在於 ...
  • 一個.NET內置依賴註入的小型強化版
    前言 .NET生態中有許多依賴註入容器。在大多數情況下，微軟提供的內置容器在易用性和性能方面都非常優秀。外加ASP.NET Core預設使用內置容器，使用很方便。 但是筆者在使用中一直有一個頭疼的問題：服務工廠無法提供請求的服務類型相關的信息。這在一般情況下並沒有影響，但是內置容器支持註冊開放泛型服 ...
  • WPF隨筆收錄-DataGrid固定右側列
    一、前言 在項目開發過程中，DataGrid是經常使用到的一個數據展示控制項，而通常表格的最後一列是作為操作列存在，比如會有編輯、刪除等功能按鈕。但WPF的原始DataGrid中，預設只支持固定左側列，這跟大家習慣性操作列放最後不符，今天就來介紹一種簡單的方式實現固定右側列。（這裡的實現方式參考的大佬 ...
所有分類