逻辑式编程语言极简实现（使用C#） - 3. 运行原理

本系列前面的文章：

• 逻辑式编程语言极简实现（使用C#） - 1. 逻辑式编程语言介绍
• 逻辑式编程语言极简实现（使用C#） - 2. 一道逻辑题：谁是凶手

次日，好为人师的老明继续开讲他的私人课堂。

“今天讲NMiniKanren的运行原理。”老明敲了敲白板，开始涂画代码，“咱们从一个喜闻乐见的例子开始。”

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, x), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));

“这题我会了！”小皮在例子下边写下答案：

[(1 1), (1 b), (2 2), (2 b)]

看到小皮没把昨天的知识忘光，老明略感欣慰：“不错。你这个答案是怎么算出来的呢？”

“呃……就是那个……”小皮突然卡壳了。这种问题就比如几何证实题，明明一眼就能看出来的两条垂直线，真下手证实却发现还挺不容易。小皮抓了几把头发，总算理出一缕思绪：“大概就是找出全部条件可能的组合……而后算一下解……”小皮一边说，一边在白板上写着：

• x == 1
  • y == x => (x y) == (1 1)
  • y == "b" => (x y) == (1 "b")
• x == 2
  • y == x => (x y) == (2 2)
  • y == "b" => (x y) == (2 "b")

“嗯，其实你已经知道怎么算出答案来了。只是对于其中的细节还不甚明了。咱们接下来要作的事要理清楚这个计算过程，获得一个每一步均可以由计算机明确执行的算法。

“这个算法其实就是你所说这样，找出全部可能的条件组合。每组条件组合能够求出一个解，也可能自相矛盾从而无解。因为NMiniKanren中的条件都是相等条件，因此一组条件组合能够看做一个替换（Substitution）。一个替换能产生一个解，或者无解。

“所以，只需解决下面两个问题：

1. 要在什么数据结构上按照什么顺序遍历替换。
2. 如何从替换中算出一个解，或者判断其无解。”

遍历分支

首先，咱们要从代码构造出一个数据结构（其实就是一张图）。这个数据结构可以按照必定的顺序进行遍历，并依次生成替换。

例子中的代码使用到了Eq、Any和All这三种构造目标的方法。下面分别探讨怎样从这三种方法构造出咱们须要的数据结构来。

Eq

“k.Eq(a, b)构造的目标是什么意思呢？”老明以一个看似平凡的问题开头。

“简单，意思就是a要等于b这个条件。”

“孤立地看，是这样。可是考虑到上下文，更精确地说应该是，在上下文的基础上追加a等于b这个条件。”

小皮有点不解：“emm……多了‘追加’有什么不一样呢？”

“从文字上看，多了‘追加’后，目标的解释从一种名词（一组条件）变成了动词（追加条件）。这样一来，目标不只表达了一组条件，同时也表达了这些条件如何跟上下文结合。就Eq的状况来讲，这个结合方式是‘追加’。而Any和All会有其余结合方式。”

“虽然还不是很明白，我想这个要等Any和All的状况一块儿对比才能清晰起来。我还另外有个问题，上下文指的是什么？”

“狭义地说，上下文是解释器运行到这一条代码时，已执行的代码生成的替换。

上下文 <-> 一个替换 <-> 一组条件

“广义上看，上下文还应该包含回溯分支等控制信息，不过目前咱们先忽略这些。

“综合起来，按照对Eq目标的解释，咱们能够用下图来表示这个目标。”

Any（或）

“接着看Any。按照上面的讨论，咱们要怎么解释Any目标呢？”老明继续发问。

“解释目标要说清楚两个方面：名词（什么条件）和动词（如何与上下文结合）。以一开始的例子中的k.Any(k.Eq(x, 1), k.Eq(x, 2))为例。名词方面天然就是x等于1和x等于2两个条件了，不过这两个条件是‘或’的关系。动词方面，应该是从上下文分岔出两个分支，一个分支追加x等于1这个条件，另外一个分支追加x等于2这个条件。”

“很好。也就是说，和Eq不一样，Any操做和上下文结合后，会生成多个替换。”老明赞许地点点头，“它把参数的分支都放在一块儿，就像加法似的。用图表示的话，就像下面这样。”

All（与）

“最后是All……”

“这个我也会了！”小皮打断老明，“k.All(a, b)名词上表示条件a且条件b；动词上表示上下文先追加a，再追加b。”

“你说的太笼统了。a和b可能都有多个分支，这种状况下怎么作？”老明接着问道。

小皮想了想一开始作的例子，答道：“这种状况要取全部组合，也就是a的分支和b的分支两两组合！最后分支数量等于a分支数量乘以b分支数量。”

“很好。若是Any类比加法，那么All类比的是乘法。下面这图描述了开头例子中的All方法的结合过程。

“这是个有向图，每条边表示一次追加条件的过程。每条从开始节点（上下文）到结尾的路径，上面的节点组合起来就是一个替换。遍历全部路径，咱们就遍历了全部替换。而遍历的顺序，就是解释器输出结果的顺序。”

Anyi

接下来咱们还能够来看看Anyi。

普通的Any使用的普通的树结构遍历顺序：

而Anyi以交替的顺序遍历分支：

Alli相似采用交替的顺序遍历，这里就再也不画了（主要是很差画，懒）。

再看目标（Goal）

上一篇主要从构造目标的角度出发，介绍了不一样方式构造出来的目标。为了实现NMiniKanren的解释器，咱们须要更加深刻地了解在解释器的实现中，Goal是什么类型。

在前面的讨论中，咱们知道，目标的含义是对上下文/一个替换按照某种方式追加一些条件，返回零个、一个或多个替换——Eq返回一个；Any和All可能返回多个；另外前面没讨论到的Fail会返回零个。

从这个描述不难看出，最方便表述目标类型的是一个单参数函数，其参数是一个替换，返回值是替换的枚举，至关于C#中的Enumerable<替换>，也能够说是一个替换的流（Stream）。

Goal: (替换) -> Stream<替换>

Goal(替换)这个函数调用的含义是把Goal包含的条件，追加到替换上，返回一系列（由于可能有分支，就会变成多个）的替换。

“为何不直接用List呢？”小皮又发问了。

“由于不少状况下，分支数量会不少，甚至是无穷多，而咱们只须要挨个取前面几个结果就够了。这种状况下使用List会极大下降解释器效率，甚至形成死循环。”

递归的状况

“略。”

“啥？”小皮瞪了下眼。

“懒得画，留着思考吧。”

替换求解

“生成替换后，剩下的就是求解了。

“替换求解的方法很简单，就是应用一下小学时学过的代入消元法。来，看看这个怎么解。”老明一边说一边写下例题：

(1) y == x
(2) q == (x y)
(3) x == 1

毕竟是小学难度的题目，小皮看了一眼，立刻就有了解法：“x等于1是肯定的了，把(3)代入(1)后，y也等于1。把(1)和(3)都代入(2)，获得q等于(1 1)。”

“解是求出来了，不过你以为你这个步骤有通用性吗？”老明虚着眼说，“计算机能自觉地使用你这个蛇皮顺序吗？”

“呃……”小皮陷入沉思。判断代入顺序的规则彷佛还挺麻烦的。或者简单粗暴按照全部顺序都代入一遍？

“其实没想象中复杂，按顺序代入一遍，再反过来代入一遍，就OK了。”

按顺序代入

把(1)代入(2)(3)：

(1) y == x
(2) q == (x x)
(3) x == 1

把(2)代入(3)：

(1) y == x
(2) q == (x x)
(3) x == 1

在解释器实现中，条件是一条一条追加上来的。能够每次追加条件的时候，将已有的条件代入新条件，这样就把这一步化解到生成替换的过程当中了。

加入条件(1) y == x:

(1) y == x

加入条件(2) q == (x y):

(1) y == x
(2) q == (x x)

加入条件(3) x == 1:

(1) y == x
(2) q == (x x)
(3) x == 1

按相反顺序代入

把(3)代入(2)(1)：

(1) y == 1
(2) q == (1 1)
(3) x == 1

把(2)代入(1)：

(1) y == 1
(2) q == (1 1)
(3) x == 1

搞定！

这只是个简单的例子。实际状况还可能会出现无解、自由变量以及死循环等状况。这里就很少赘述了。

再议“非”运算

“如今能看出NMiniKanren为何不支持‘非’运算了吗？”

小皮认真想了一会，说：“岂止不支持‘非’，‘大于’和‘小于’这些也不行吧。按照代入消元法，NMiniKanren只支持相等条件。”。

“那若是要支持这些运算应该怎么作呢？”

“要拓展条件的类型。除了相等条件，还要有不相等条件等。响应的求解算法也要有所变化。”

“没错。改动虽然不大，可是代码看起来会混乱得多。因此以教学为目的的话，就不支持这些了。”

小结

不知不觉时间已到了喜闻乐见的午饭时间，因而老明总结道：“虽然尚未落地成代码，但运行原理算是弄清楚了。关键点就两个:

1. 要在什么数据结构上按照什么顺序遍历替换。
2. 如何从替换中算出一个解，或者判断其无解。

“第一点，咱们从代码构造了一张图。该图的每条路径对应一个替换，遍历路径的顺序就是遍历替换的顺序。同时也明确了目标Goal的类型。

“第二点，咱们使用代入消元法，来回两遍代入解出了全部未知量。”

“接下来能够写代码实现NMiniKanren解释器了吧。”理解了原理后，小皮的十条手指已经饥渴难耐，蚯蚓似的扭动着。

“不着急，下午还要先讲一个编程小技巧，而后就能够开搞了。”