每次点一下按钮，就相当于调用了一次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<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的原理：
- NMiniKanren代码描述的是一个Goal。Goal是一个替换到Stream的函数。
- 从NMiniKanren代码可以构建一张描述了条件关系的图。每条路径对应一个替换，使用流计算模式可以很巧妙地实现对所有路径的遍历。
- 使用代入消元法求解未知量。
另外NMiniKanren毕竟只是一门教学级的语言，实用上肯定一塌糊涂，说难听点也就是个玩具。我们学习的重点不在于NMiniKanren，而在于实现NMiniKanren的过程中所用到的技术和思想。掌握了这些方法后，可以根据自己的需要进行优化或扩展，或者将这些方法应用到其他问题上。
神奇！小皮瞪着眼睛摸摸脑袋，以前觉得宛若天书般的逻辑式编程语言就这么学完了，还包括了解释器的实现。
认真学习了一天半的效果还是不错了。嘿嘿。老明欣慰地拍了拍小皮的肩膀，微微笑道，世上无难事，只怕有心人。恰好今天周五了，周末就来公司把这两天落下的工作补完吧。
小皮：？？？
PS：最后，用《The Reasoned Schemer》里的两页实现镇楼。俗话说得好，C#只是恰饭，真正的快乐还得看Scheme/Lisp。
原创文章，作者：guozi，如若转载，请注明出处：https://www.sudun.com/ask/82441.html
