本系列前面的文章:
第二天,好为人师的老明继续开讲他的私人课堂。
“今天讲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中的条件都是相等条件,所以一组条件组合可以看作一个)。
再看目标(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只支持相等条件。”。
“那如果要支持这些运算应该怎么做呢?”
“要拓展条件的类型。除了相等条件,还要有不相等条件等。响应的求解算法也要有所变化。”
“没错。改动虽然不大,但是代码看起来会混乱得多。所以以教学为目的的话,就不支持这些了。”
小结
不知不觉时间已到了喜闻乐见的午餐时间,于是老明总结道:“虽然还没有落地成代码,但运行原理算是弄清楚了。关键点就两个:
- 要在什么数据结构上按照什么顺序遍历替换。
- 如何从替换中算出一个解,或者判断其无解。
“第一点,我们从代码构造了一张图。该图的每条路径对应一个替换,遍历路径的顺序就是遍历替换的顺序。同时也明确了目标Goal的类型。
“第二点,我们使用代入消元法,来回两遍代入解出了所有未知量。”
“接下来可以写代码实现NMiniKanren解释器了吧。”理解了原理后,小皮的十条手指已经饥渴难耐,蚯蚓似的扭动着。
“不着急,下午还要先讲一个编程小技巧,然后就可以开搞了。”