邏輯式編程語言極簡實現（使用C#） - 1. 邏輯式編程語言介紹

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

相信很多朋友對於邏輯式編程語言，都有一種最熟悉的陌生人的感覺。一方面，平時在書籍、在資訊網站，偶爾能看到一些吹噓邏輯式編程的話語。但另一方面，也沒見過周圍有人真正用到它（除了SQL）。 本系列將儘可能簡潔地說明邏輯式編程語音的原理，並實現一門簡單的邏輯式編程語言。考慮到C#的用戶較多，因此選擇用C#... ...


相信很多朋友對於邏輯式編程語言，都有一種最熟悉的陌生人的感覺。一方面，平時在書籍、在資訊網站，偶爾能看到一些吹噓邏輯式編程的話語。但另一方面，也沒見過周圍有人真正用到它（除了SQL）。

遙記當時看《The Reasoned Schemer》（一本講邏輯式編程語言的小人書），被最後兩頁的解釋器實現驚艷到了。看似如此複雜的計算邏輯，其實現竟然這麼簡潔。不過礙於當時水平有限，也就囫圇吞棗般看了過去。後來有一天，不知何故腦子靈光一閃，把圖遍歷和流計算模式聯繫在一起，瞬間明白了《The Reasoned Schemer》中的做法。動手寫了寫代碼，果然如此，短短兩百來行代碼，就完成瞭解釋器的實現，才發現原來如此簡單。很多時候，並非問題本身有多難，只是沒有想到正確的方法。

本系列將儘可能簡潔地說明邏輯式編程語音的原理，並實現一門簡單的邏輯式編程語言。考慮到C#的用戶較多，因此選擇用C#來實現。實現的這門語言就叫NMiniKanren。文章總體內容如下：

  • NMiniKanren語言介紹
    • 語言基礎
    • 一道有趣的邏輯題：誰是凶手
  • NMiniKanren運行原理
    • 構造條件關係圖，遍歷分支
    • 代入消元法解未知量
  • 實現NMiniKanren
    • 流計算模式簡介
    • 代入消元法的實現
    • 遍歷分支的實現

故事從兩個正在吃午餐的程式員說起。

老明和小皮是就職於同一家傳統企業的程式員。這天，兩人吃著午餐。老明邊吃邊刷著抖音，鼻孔時不時噴出幾條米粉。

小皮是一臉麻木地刷著求職網和資訊網，忽然幾個大字映入眼底：《新型邏輯式編程語言重磅出世，即將顛覆IT界！》小皮一陣好奇，往下一翻，結果接著的是一些難懂的話，什麼“一階邏輯”，什麼“合一演算法”，以及鬼畫符似的公式之類。

小皮看得索然無味，但被勾引起來的對邏輯式編程的興趣仿佛澳洲森林大火一樣難以平息。於是伸手拍下老明高舉手機的左手，問道：“嘿！邏輯式編程有瞭解過麽？是個啥玩意兒？”

“邏輯式編程啊……嘿嘿，前段時間剛好稍微瞭解了一下。”老明鼻孔朝天吸了兩口氣，“我說的稍微瞭解，是指實現了一門邏輯式編程語言。”

“不愧是資深老IT，瞭解也比別人深入一坨坨……”

“也就比你早來一年好不好……我是一邊看一本奇書一邊做的。Dan老師（Dan Friedman）寫的《The Reasoned Schemer》。這本書挺值得一看的，書中使用一門教學用的邏輯式編程語言，講解這門語言的特性、用法、以及原理。最後還給出了這門語言的實現。核心代碼只用了兩頁紙。

“所謂邏輯式編程，從使用上看是把聲明式編程發揮到極致的一種編程範式。普通的編程語言，大部分還是基於命令式編程，需要你告訴機器每一步執行什麼指令。而邏輯式編程的理念是，我們只需要告訴機器我們需要的目標，機器會根據這個目標自動探索執行過程。

“邏輯式編程的特點是可以反向運行。你可以像做數學題一樣，聲明未知量，列出方程，然後程式會為你求解未知量。”

“挺神奇的。聽起來有點像AI編程。不過這麼高級的東西怎麼沒有流行起來？感覺可以節省不少人力。”小皮忽然有種飯碗即將不保的感覺。

“嘿嘿……想得美。其實邏輯式編程，既不智能，也不好用。你回憶一下你中學的時候是怎麼解方程組的？”

“嗯……先盯一會方程組，看看它長得像不像有快捷解法的樣子。看不出來的話就用代入法慢慢算。這和邏輯式編程有什麼關係？”

“邏輯式編程並不智能，它只是把某種類似代入法的通用演算法內置到解釋器里。邏輯式編程語言寫的程式運行時，不過是根據通用演算法進行求解而已。它不像人一樣會去尋找更快捷的方法，同時也不能解決超綱問題。

“而且邏輯式編程語言的學習成本也不低。如果你要用好這門語言，你得把它使用的通用演算法搞清楚。雖然你寫的聲明式的代碼，但內心要時刻清楚程式的執行過程。如果你拿它當個黑盒來用，那很可能你寫出來的程式的執行效率會非常低，甚至跑出一些莫名其妙的結果。”

“哦哦，要學會用它，還得先懂得怎麼實現它。這學習成本還挺高的。”小皮跟著吐槽，不過他知道老明表明上看似嫌棄邏輯式編程的實用性，私底下肯定玩得不亦樂乎，並且也喜歡跟別人分享。於是小皮接著道：“雖然應該是用不著，但感覺挺有意思的，再仔細講講唄。天天寫CRUD，腦子都淡出個鳥了。”

果然老明坐直起來：“《The Reasoned Schemer》用的這門邏輯式編程語言叫miniKanren，用Scheme/Lisp實現的。去年給你安利過Scheme了，現在掌握得怎麼樣？”

“一竅不通……”小皮大窘。去年到現在，小皮一直很忙，並沒有自學什麼東西。如果沒有外力驅動的話，他還將一直忙下去。

“果然如此。所以我順手也實現了個C#魔改版本的miniKanren。就叫NMiniKanren。我把NMiniKanren實現為C#的一個DSL。這樣的好處是方便熟悉C#或者Java的人快速上手；壞處是DSL會受限於C#語言的能力，代碼看起來沒有Scheme版那麼優雅。”老明用左手做了個打引號的動作，“先從簡單的例子開始吧。比如說，有個未知量q，我們的目標是讓q等於5或者等於6。那麼滿足條件的q值有哪些？”

“不就是5和6麽……這也太簡單了吧。”

“Bingo！”老明打了個響指，“我們先用簡單的例子看看代碼結構。”只見老明兩指輕輕夾住一隻筷子，勾出幾條米粉，快速在桌上擺出如下代碼：

// k提供NMiniKanren的方法，q是待求解的未知變數。
var res = KRunner.Run(null /* null表示輸出所有可能的結果 */, (k, q) =>
{
    // q == 5 或者 q == 6
    return k.Any(
        k.Eq(q, 5),
        k.Eq(q, 6));
});
KRunner.PrintResult(res);  // 輸出結果：[5, 6]

“代碼中，KRunner.Run用於運行一段NMiniKanren代碼，它的聲明如下。”老明繼續撥動米粉：

public class KRunner
{
    public static IList<object> Run(int? n, Func<KRunner, FreshVariable, Goal> body)
    {
        ...
    }
}

“其中，參數n是返回結果的數量限制，n = null表示無限制；參數body是一個函數：

  • 函數的第一個參數是一個KRunner實例，用於引用NMiniKanren方法；
  • 函數的第二個參數是我們將要求解的未知量；
  • 函數的函數體是我們編寫的NMiniKanren代碼；
  • 函數的返回值為需要滿足的約束條件。

“接著我們看函數體的代碼。k.Eq(q, 5)表示q需要等於5，k.Eq(q, 6)表示q需要等於6，k.Any表示滿足至少一個條件。整段代碼的意思為：求所有滿足q等於5或者q等於6的q值。顯然答案為5和6，程式的運行結果也是如此。很神奇吧？”

“你這米粉打碼的功夫更讓我驚奇……”小皮仔細看了一會，“原來如此。不過這DSL的語法確實看著比較累。”

“主要是我想做得簡單一些。其實使用C#的Lambda表達式也可以實現像……”老明勾出幾條米粉擺出q == 5 || q == 6表達式，“……這樣的語法，不過這樣會增加NMiniKanren實現的複雜度。況且這無非是首碼表達式或中綴表達式這種語法層面的差別而已，語義上並沒有變化。學習應先抓住重點，花里胡哨的東西可以放到最後再來琢磨。”

“嗯嗯。KRunner.Run里這個null的參數是做什麼用的呢？”

“KRunner.Run的第一個參數用來限制輸出結果的數量。null表示輸出所有可能的結果。還是上面例子的條件，我們改成限制只輸出1個結果。”小皮用筷子改了下代碼：

// k提供NMiniKanren的方法，q是待求解的未知變數。
var res = KRunner.Run(1 /* 輸出1個結果 */, (k, q) =>
{
    // q == 5 或者 q == 6
    return k.Any(
        k.Eq(q, 5),
        k.Eq(q, 6));
});
KRunner.PrintResult(res);  // 輸出結果：[5]

“這樣程式只會輸出5一個結果。在一些包含遞歸的代碼中，可能會有無窮多個結果，這種情況下需要限制輸出結果的數量來避免程式不會終止。”

“原來如此。不過這個例子太簡單了，有沒有其他更好玩的例子。”

老明喝下一口湯，說：“好。時間不早了，我們回公司找個會議室慢慢說。”

NMiniKanren支持的數據類型

到公司後，老明的講課開始了……

首先，要先明確NMiniKanren支持的數據類型。後續代碼都要基於數據類型來編寫，所以規定好數據類型是基礎中的基礎。

簡單起見，NMiniKanren只支持四種數據類型：

  • string：就是一個普普通通的值類型，僅有值相等判斷。
  • int：同string。使用int是因為有時候想少寫兩個雙引號……
  • KPair：二元組。可用來構造鏈表及其他複雜的數據結構。如果你學過Lisp會對這個數據結構很熟悉。下麵詳細說明。
  • null：這個類型只有null一個值。表示空引用或者空數組。

KPair類型

KPair的定義為：

public class KPair
{
    public object Lhs { get; set; }
    public object Rhs { get; set; }
    
    // methods
    ...
}

KPair除了用作二元組（其實是最少用的）外，更多的是用來構造鏈表。構造鏈表時，約定一個KPair作為一個鏈表的節點，Lhs為元素值，Rhs為一下個節點。當Rhs為null時鏈表結束。空鏈表用null表示。

public static KPair List(IEnumerable<object> lst)
{
    var fst = lst.FirstOrDefault();
    if (fst == null)
    {
        return null;
    }
    return new KPair(fst, List(lst.Skip(1)));
}

使用null表示空鏈表其實並不合適，這裡純粹是為了簡單而偷了個懶。

我們知道，很多複雜的數據結構都是可以通過鏈表來構造的。所以雖然NMiniKanren只有三種數據類型，但可以表達很多數據結構了。

這時候小皮有疑問了：“C#本身已經自帶了List等容器了，為什麼還要用KPair來構造鏈表？”

“為了讓底層儘可能簡潔。”老明說道，“我們都知道，程式本質上分為數據結構和演算法。演算法是順著數據結構來實現的。簡潔的數據結構會讓演算法的實現顯得更清晰。相比C#自帶的List，使用KPair構造的鏈表更加清晰簡潔。按照構造的方式，我們的鏈表定義為：

  1. 空鏈表null；
  2. 或者是非空鏈表。它的第一個元素為Lhs，並且Rhs是後續的鏈表。

“鏈表相關的演算法都會順著定義的這兩個分支實現：一個處理空鏈表的分支，一個處理非空鏈表的遞歸代碼。比如說判斷一個變數是不是鏈表的方法：

public static bool IsList(object o)
{
    // 空鏈表
    if (o == null)
    {
        return true;
    }
    // 非空鏈表
    if (o is KPair p)
    {
        // 遞歸
        return IsList(p.Rhs);
    }
    // 非鏈表
    return false;
}

“以及判斷一個元素是不是在鏈表中的方法：

public static bool Memeber(object lst, object e)
{
    // 空鏈表
    if (lst == null)
    {
        return false;
    }
    // 非空鏈表
    if (lst is KPair p)
    {
        if (p.Lhs == null && e == null || p.Lhs.Equals(e))
        {
            return true;
        }
        else
        {
            // 遞歸
            return Memeber(p.Rhs, e);
        }
    }
    // 非鏈表
    return false;
}

“數據類型明確後，接下來我們來看看NMiniKanren能做什麼。”

目標（Goal）

編寫NMiniKanren代碼是一個構造目標（Goal類型）的過程。NMiniKanren解釋器運行時將求解使得目標成立的所有未知量的值。

顯然，有兩個平凡的目標：

  • k.Succeed：永遠成立，未知量可取任意值。
  • k.Fail：永遠不成立，無論未知量為何值都不成立。

其中k是KRunner的一個實例。C#跟Java一樣不能定義獨立的函數和常量，所以我們DSL需要的函數和常量就都定義為KRunner的方法或屬性。後面不再對k進行覆述。

一個基本的目標是k.Eq(v1, v2)。這也是NMiniKanren唯一一個使用值來構造的目標，它表示值v1和v2應該相等。也就是說，當v1與v2相等時，目標k.Eq(v1, v2)成立；否則不成立。

這裡的相等，指的是值相等：

  • 不同類型不相等。
  • string類型相等當且僅當值相等。
  • KPair類型相等當且僅當它們的Lhs相等且Rhs相等。

從KPair相等的定義，可以推出由KPair構造的數據結構（比如鏈表），相等條件為當且僅當它們結構一樣且對應的值相等。

接下來我們看幾個例子。

等於一個值

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Eq(q, 5);
}));  // 輸出[5]

直接q等於5。

等於一個鏈表

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Eq(q, k.List(1, 2));
}));  // 輸出[(1 2)]

k.List(1, 2)相當於new KPair(1, new KPair(2, null))，用來快速構造鏈表。

鏈表間的相等

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Eq(k.List(1, q), k.List(1, 2));
}));  // 輸出[2]

這個例子比較像一個方程了。q匹配k.List(1, 2)的第二項，也就是2。

無法相等的例子

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Eq(k.List(2, q), k.List(1, 2));
}));  // 輸出[]

由於k.List(2, q)的第一項和k.List(1, 2)的第一項不相等，所以這個目標無法成立，q沒有值。

不成立的例子

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Fail;
}));  // 輸出[]

目標無法成立，q沒有值。

永遠成立的例子

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Succeed;
}));  // 輸出[_0]

目標恆成立，q可取任意值。輸出_0表示一個可取任意值的自由變數。

更多構造目標的方式

目標可以看作布爾表達式，因此可以通過“與或非”運算，用簡單的目標構造成複雜的“組合”目標。我們把被用來構造“組合”目標的目標叫做該“組合”目標的子目標。

定義未知量

在前面的例子中，我們只有一個未知量q。q既是未知量，也是程式輸出。

在處理更複雜的問題時，通常需要定義更多的未知量。定義未知量的方法是k.Fresh：

// 定義x, y兩個未知量
var x = k.Fresh()
var y = k.Fresh()

新定義的未知量和q一樣，可以用來構造目標：

// x == 2
k.Eq(x, 2)
// x == y
k.Eq(x, y)

與

使用“與”運算組合的目標，僅當所有子目標成立時，目標才成立。

使用方法k.All來構造“與”運算組合的目標。

var g = k.All(g1, g2, g3, ...)

當且僅當g1, g2, g3, ......，都成立時，g才成立。

特別的，空子目標的情況，即k.All()，恆成立。

例

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.All(
        k.Eq(q, 1),
        k.Eq(q, 2));
}));  // 輸出[]

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.Eq(x, 1),
        k.Eq(y, x),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(1 1)]

或

使用“或”運算組合的目標，只要一個子目標成立時，目標就成立。

使用方法k.Any來構造“或”運算組合的目標。

var g = k.Any(g1, g2, g3, ...)

當g1, g2, g3, ......中至少一個成立，g成立。

特別的，空子目標的情況，即k.Any()，恆不成立。

例

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Any(
        k.Eq(q, 5),
        k.Eq(q, 6));
}));  // 輸出[5, 6]

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.Any(k.Eq(x, 5), k.Eq(y, 6)),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(5 _0), (_0 6)]

非？

MiniKanren（以及NMiniKanren）不支持“非”運算。支持“非”會讓miniKanren的實現複雜很多。

這或許令人驚訝。“與或非”在邏輯代數中一直像是連體嬰兒似的扎堆出現。並且“非”運算是單目運算符，看起來應該更簡單。

然而，“與”和“或”運算是在已知的兩（多）個集合中取交集或者並集，結果也是已知的。而“非”運算則是把一個已知的集合映射到可能未知的集合，遍歷“非”運算的結果可能會很久或者就是不可能的。

對於基於圖搜索和代入法求解的miniKanren來說，支持“非”運算需要對核心的數據結構和演算法做較大改變。因此以教學為目的的miniKanren沒有支持“非”運算。

不過，在一定程度上，也是有不完整替代方法的。

If（這個比較奇葩，可以先跳過）

If是一個特殊的構造目標的方式。對應《The Reasoned Schemer》中的conda。

var g = k.If(g1, g2, g3)

如果g1且g2成立，那麼g成立；否則當且僅當g3成立時，g成立。

這個和k.Any(k.All(g1, g2), g3)很像，但他們是有區別的：

  • k.Any(k.All(g1, g2), g3)會解出所有讓k.All(g1, g2)或者g3成立的解
  • k.If(g1, g2, g3)如果k.All(g1, g2)有解，那麼只給出使k.All(g1, g2)成立的解；否則再求使得g3成立的解。

也可以說，If是短路的。

這麼詭異的特性有什麼用呢？

它可以部分地實現“非”運算的功能：

k.If(g, k.Fail, k.Succeed)

這個這裡先不詳細展開了，後面用到再說。

控制輸出順序

這是一個容易被忽略的問題。如果程式需要求出所有的解，那麼輸出順序影響不大。但是一些情況下，求解速度很慢，或者解的數量太多甚至無窮，這時只求前幾個解，那麼輸出的內容就和輸出順序有關了。

因為miniKanren以圖遍歷的方式來查找問題的解，所以解的順序其實也是解釋器運行時遍歷的順序。先看如下例子：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.Any(k.Eq(x, 1), k.Eq(x, 2)),
        k.Any(k.Eq(y, "a"), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(1 a), (1 b), (2 a), (2 b)]

有兩個未知變數x和y，x可能的取值為1或2，y可能的取值為a或b。可以看到，程式查找解的順序為：

  • x值為1
    • y值為a，q=(1 a)
    • y值為b，q=(1 b)
  • x值為2
    • y值為a，q=(2 a)
    • y值為b，q=(2 b)

如果要改變這個順序，我們有一個交替版的“與”運算k.Alli：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.Alli(
        k.Any(k.Eq(x, 1), k.Eq(x, 2)),
        k.Any(k.Eq(y, "a"), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(1 a), (2 a), (1 b), (2 b)]

不過這個交替版也不是交替得很漂亮。下麵增加x可能的取值到3個：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.Alli(
        k.Any(k.Eq(x, 1), k.Eq(x, 2), k.Eq(x, 3)),
        k.Any(k.Eq(y, "a"), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(1 a), (2 a), (1 b), (3 a), (2 b), (3 b)]

同樣，“或”運算也有交替版。

正常版：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Any(
        k.Any(k.Eq(q, 1), k.Eq(q, 2)),
        k.Any(k.Eq(q, 3), k.Eq(q, 4)));
}));  // 輸出[1, 2, 3, 4]

交替版：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    return k.Anyi(
        k.Any(k.Eq(q, 1), k.Eq(q, 2)),
        k.Any(k.Eq(q, 3), k.Eq(q, 4)));
}));  // 輸出[1, 3, 2, 4]

後面講到miniKanren實現原理時會解釋正常版、交替版為什麼會是這種表現。

遞歸

無遞歸，不編程！

遞歸給予了程式語言無限的可能。NMiniKanren也是支持遞歸的。下麵我們實現一個方法，這個方法構造的目標要求指定的值或者未知量是一個所有元素都為1的鏈表。

錯誤的示範

一個值或者未知量的元素都為1，用遞歸的方式表達是：

  1. 它是一個空鏈表
  2. 或者它的第一個元素是1，且剩餘部分的元素都為1

直譯為代碼就是：

public static Goal AllOne_Wrong(this KRunner k, object lst)
{
    var d = k.Fresh();
    return k.Any(
        // 空鏈表
        k.Eq(lst, null),
        // 非空
        k.All(
            k.Eq(lst, k.Pair(1, d)),  // 第一個元素是1
            k.AllOne_Wrong(d)));  // 剩餘部分的元素都是1
}

直接運行這段代碼，死迴圈。

為什麼呢？因為我們直接使用C#的方法來定義函數，C#在構造目標的時候，會運行最後一行的k.AllOne_Wrong(d)，於是就陷入死迴圈了。

正確的做法

為了避免死迴圈，在遞歸調用的地方，需要用k.Recurse方法特殊處理一下，讓遞歸的部分變為惰性求值，防止直接調用：

public static Goal AllOne(this KRunner k, object lst)
{
    var d = k.Fresh();
    return k.Any(
        k.Eq(lst, null),
        k.All(
            k.Eq(lst, k.Pair(1, d)),
            k.Recurse(() => k.AllOne(d))));
}

隨便構造兩個問題運行一下：

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.AllOne(k.List(1, x, y, 1)),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[(1 1)]

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.AllOne(k.List(1, x, y, 0)),
        k.Eq(q, k.List(x, y)));
}));  // 輸出[]

k.Recurse這種處理方法其實是比較醜陋而且不好用的。特別是多個函數相互調用引起遞歸的情況，很可能會漏寫k.Recurse導致死迴圈。

聽到這裡，小皮疑惑道：“這個有點醜誒。剛剛網上瞄了下《The Reasoned Schemer》，發現人家的遞歸併不需要這種特殊處理。看起來直接調用就OK了，跟普通程式沒啥兩樣，很美很和諧。”

“因為《The Reasoned Schemer》使用Lisp的巨集實現的miniKanren，巨集的機制會有類似惰性計算的效果。”老明用擦白板的抹布拍了下小皮的腦袋，“可惜你不會Lisp。如果你不努力提升自己，那醜一點也只能將就著看了。”

關於數值計算

MiniKanren沒有直接支持數值計算。也就是說，miniKanren不能直接幫你解像2 + x = 5的這種方程。如果要直接支持數值計算，需要實現很多數學相關的運算和變換，會讓miniKanren的實現變得非常複雜。MiniKanren是教學性質的語言，只支持了最基本的邏輯判斷功能。

“沒有‘直接’支持。”小皮敏銳地發現了關鍵，“也就是可以間接支持咯？”

“沒錯！你想想，0和1是我們支持的符號，與和或也是我們支持的運算符！”老明興奮起來了。

“二進位？”

“是的！任何一本電腦組成原理教程都會教你怎麼做！這裡就不多說了，你可以自己回去試一下。”

“嗯嗯。我以前這門課學得還不錯，現在還記得大概是先實現半加器和全加器，然後構造加法器和乘法器等。”小皮幹勁十足，從底層開始讓他想起了小時候玩泥巴的樂趣。

“而且用miniKanren實現的不是一般的加法器和乘法器，是可以反向運行的加法器和乘法器。”

“有意思，晚上下班回去就去試試。”小皮真心地說。正如他下班回家躺床上後，就再也不想動彈一樣真心實意。

（註：《The Reasoned Schemer》第7章、第8章會講到相關內容。）

小結

“好了，NMiniKanren語言的介紹就先說到這裡了。”老明拍了拍手，看了看前面的例子，撇了撇嘴，“以C#的DSL方式實現出來果然醜很多，語法上都不一致了。不過核心功能都還在。”

“接下來就是最有意思的部分，NMiniKanren的原理了吧？”

“是的。不過在繼續之前，還有個問題。”

“啥問題？”

“中午米線都用來打碼了。現在肚子餓了，你要請我吃下午茶。”

NMiniKanren的源碼在：https://github.com/sKabYY/NMiniKanren

示例代碼在：https://github.com/sKabYY/NMiniKanren/tree/master/NMiniKaren.Tests


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

-Advertisement-
Play Games
更多相關文章
  • Java自學課程視頻教程，從入門到精通
    最近也有很多人來向小編"請教"，他們大都是一些剛入門的新手，還不瞭解這個行業，也不知道從何學起，開始的時候非常迷茫，實在是每天回覆很多人也很麻煩，所以在這裡小編總結一些基礎課程： 基礎階段 首先是基礎階段，在基礎階段，我們必須掌握Java基礎，Mysql資料庫，Oracle資料庫，JDBC，Linu ...
  • 編程基礎之Java中繼承和多態的理解
    JAVA中繼承和多態的理解 繼承的概念 繼承是java面向對象編程技術的一塊基石，因為它允許創建分等級層次的類。 繼承就是子類繼承父類的特征和行為，使得子類對象（實例）具有父類的實例域和方法，或子類從父類繼承方法，使得子類具有父類相同的行為。 類的繼承格式 在Java中通過extends關鍵字可以申 ...
  • Springboot自定義打包
    學習記錄1--Springboot的Maven自定義打包 在以往的開發中,Springboot應用預設打成一個jar,雖然方便但是會有很多問題,比如不方便修改配置文件,修改一個處代碼就要更新整包等等,而maven中也有這樣的插件可以給我們提供幫助 複製引用依賴插件 <plugin> <groupId ...
  • 初探numpy——切片和索引
    切片 import numpy as np # 使用切片參數start:stop:step來進行切片操作 a_array=np.arange(10) print(a_array,'\n') b_array=a_array[1:10:2] print(b_array,'\n') c_array=a_a ...
  • 數據結構與演算法(二) 線性表一
    線性表： 定義：由零個或多個數據元素組成的有限序列。 首先他是一個序列，也就是說元素之間是有先來後到 若元素存在多個，則第一個元素無前驅，最後一個元素無後繼，其他元素有且只有一個前驅和後繼 另外，線性表強調是有限的。 數學語言的定義： 若將線性表記為(a1，...，ai-1，ai，ai+1，...a ...
  • java課程設計階段一 個人設計
    目 錄 1 選題.......................................................................................................................... 1 2 系統需求分析......... ...
  • Python開發環境Spyder介紹
    Spyder簡介 Spyder (前身是 Pydee) 是一個強大的互動式 Python 語言開發環境，提供高級的代碼編輯、交互測試、調試等特性，支持包括 Windows、Linux 和 OS X 系統。 ● 菜單欄（Menu bar）：顯示可用於操縱Spyder各項功能的不同選項。 ● 工具欄（T ...
  • Spring11——Quartz
    Quartz:定時非同步任務 任務：做什麼事情； 觸發器：定義時間； 調度器：將任務、觸發器一一對應。 實現步驟（獨立使用）： 1.jar 2.任務（service）：Job 3.測試方法：job、觸發器、調度器 scheduler.shutdown(); 立刻關閉 scheduler.shutdow ...
一周排行
    -Advertisement-
    Play Games
  • 移動開發（一）：使用.NET MAUI開發第一個安卓APP
    移動開發（一）：使用.NET MAUI開發第一個安卓APP 對於工作多年的C#程式員來說，近來想嘗試開發一款安卓APP，考慮了很久最終選擇使用.NET MAUI這個微軟官方的框架來嘗試體驗開發安卓APP，畢竟是使用Visual Studio開發工具，使用起來也比較的順手，結合微軟官方的教程進行了安卓 ...
  • wpf ToggleButton選中效果和一個登錄界面
    前言 QuestPDF 是一個開源 .NET 庫，用於生成 PDF 文檔。使用了C# Fluent API方式可簡化開發、減少錯誤並提高工作效率。利用它可以輕鬆生成 PDF 報告、發票、導出文件等。 項目介紹 QuestPDF 是一個革命性的開源 .NET 庫，它徹底改變了我們生成 PDF 文檔的方 ...
  • 彈幕樹洞項目功能新增篇
    項目地址 項目後端地址： https://github.com/ZyPLJ/ZYTteeHole 項目前端頁面地址： ZyPLJ/TreeHoleVue (github.com) https://github.com/ZyPLJ/TreeHoleVue 目前項目測試訪問地址： http://tree ...
  • 第27篇 sqlserver2022詳細安裝步驟
    話不多說，直接開乾 一.下載 1.官方鏈接下載： https://www.microsoft.com/zh-cn/sql-server/sql-server-downloads 2.在下載目錄中找到下麵這個小的安裝包 SQL2022-SSEI-Dev.exe，運行開始下載SQL server； 二. ...
  • .NET 開源高性能 MQTT 類庫
    前言 隨著物聯網（IoT）技術的迅猛發展，MQTT（消息隊列遙測傳輸）協議憑藉其輕量級和高效性，已成為眾多物聯網應用的首選通信標準。 MQTTnet 作為一個高性能的 .NET 開源庫，為 .NET 平臺上的 MQTT 客戶端與伺服器開發提供了強大的支持。 本文將全面介紹 MQTTnet 的核心功能 ...
  • Serilog文檔翻譯系列（六） - 可用的接收器、增強器、格式化輸出
    Serilog支持多種接收器用於日誌存儲，增強器用於添加屬性，LogContext管理動態屬性，支持多種輸出格式包括純文本、JSON及ExpressionTemplate。還提供了自定義格式化選項，適用於不同需求。 ...
  • 警惕 Visual Studio 屬性求值副作用導致邏輯不符合預期
    目錄簡介獲取 HTML 文檔解析 HTML 文檔測試參考文章 簡介 動態內容網站使用 JavaScript 腳本動態檢索和渲染數據，爬取信息時需要模擬瀏覽器行為，否則獲取到的源碼基本是空的。 本文使用的爬取步驟如下： 使用 Selenium 獲取渲染後的 HTML 文檔 使用 HtmlAgility ...
  • [使用目前最新版]HybridCLR6.9.0+YooAsset2.2.4實現純C# Unity熱更新方案 (一)
    1.前言 什麼是熱更新 游戲或者軟體更新時，無需重新下載客戶端進行安裝，而是在應用程式啟動的情況下，在內部進行資源或者代碼更新 Unity目前常用熱更新解決方案 HybridCLR，Xlua，ILRuntime等 Unity目前常用資源管理解決方案 AssetBundles，Addressable， ...
  • 在 ASP.NET Core Web API 中使用操作篩選器統一處理通用操作
    本文章主要是在C# ASP.NET Core Web API框架實現向手機發送驗證碼簡訊功能。這裡我選擇是一個互億無線簡訊驗證碼平臺，其實像阿裡雲，騰訊雲上面也可以。 首先我們先去 互億無線 https://www.ihuyi.com/api/sms.html 去註冊一個賬號 註冊完成賬號後，它會送 ...
  • 第28篇 如何.net中實現高效可靠數據同步api
    通過以下方式可以高效，並保證數據同步的可靠性 1.API設計 使用RESTful設計，確保API端點明確，並使用適當的HTTP方法（如POST用於創建，PUT用於更新）。 設計清晰的請求和響應模型，以確保客戶端能夠理解預期格式。 2.數據驗證 在伺服器端進行嚴格的數據驗證，確保接收到的數據符合預期格 ...
所有分類