相信很多朋友对于逻辑式编程语言，都有一种最熟悉的陌生人的感觉。一方面，平时在书籍、在资讯网站，偶尔能看到一些吹嘘逻辑式编程的话语。但另一方面，也没见过周围有人真正用到它（除了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