microKanren学习笔记
简介
之前提到逻辑编程对于区块链的Dapp编程模型非常有帮助。
我虽然很早之前也简单的学过一点Prolog，但是对其实现并没有深入的了解。
要实现一个用于Dapp框架的逻辑编程引擎，还是需要不少改动，因此有必要对其实现进行一些了解。
miniKanren是Dan Friedman在他的书《The Reasoned Schemer》中用来介绍逻辑编程的一个小巧的教学语言。其官网有相关资料和各种语言的实现。
microKanren是2013年由Dan Friedman的学生在一篇论文<µKanren: A Minimal Functional Core for Relational Programming>中提出的。对miniKanren进行了进一步的精炼，整个语言的scheme实现只有40多行（参见代码仓库）。亲自动手实现一下microKanren可谓是学习逻辑编程的最佳方法。
目标
为了便于将来理解和修改，我决定采用Rust语言，以更接近命令式语言的思路去实现。
官网上虽然有不少语言的实现，但是感觉都受到原始实现的很大影响，都是一股浓浓的lisp的味道。
参考资料
首先是看原始论文和实现。论文附带的实现虽然只有40多行，但那是得益于scheme的强大表达能力，其实里面的东西还是不少的。
看了一天，感觉对语言大概了解了，但是实现上还有很多点没弄清楚。
这时有个视频对我帮助很大。其实这个视频也没讲什么特别的东西，只是现场把原始实现写了一遍。但是通过展示这40多行代码是怎么一点一点加上来的，每一点修改解决了什么问题。而且里面还通过交互命令行在每一个步骤都展示了例子。这让我一下子就把之前的问题全都想通了。很多时候直接看最终代码，是很难理解的，但是如果看到了过程，就容易多了。
我的实现的代码仓库。
学习笔记
首先是整体印象，其实逻辑编程整体很像解代数方程组。
有多个描述等价关系的等式，里面包含一些变量。多个等式之间由逻辑连接词（and/or）连接。
运行的结果是其中每个变量的解，当然解可能有多组，表示为一个数组。
比如方程组：
x0 = 1
x1 = x0
它的解就是：
{x0 = 1; x1 = 1}
另外or关系的方程组
x0 = 5 or x0 = 6
它的解就是一个数组：
[{x0 = 5}, {x0 = 6}]
首先我们就来定义变量（Var）。
变量跟一个序号关联，比如前面的x0，x1。序号相同的变量被认为是同一个变量。
原始实现里面Var使用scheme里的vector来实现。这其实没什么特别的含义，只是为了从类型上做个区分，方便判断一个表达式是变量还是值。
在我的实现里面直接就把Var定义为一个结构。实现了Dispaly和Eq。
Value定义为一个枚举，可以是变量，也可以是一个数字（为了简化，就假定值只能取这两类）。
然后提供is_var来判断一个Value是否是Var。
接下来是Assoc。它表示了一个变量和一个值（记住这个值也有可能是一个变量）的绑定关系。
这里就直接实现为包含一个变量和一个值的结构。
Subst是一组Assoc，这里就直接实现为一个Assoc的数组。
这里有个比较重要的操作walk。
这个函数的作用是试图在一个Subst内追踪一个值对应的的非变量值。其实就是一个查询操作。
如果要查找的值本身就不是变量，那么就直接返回这个值。
如果要查找的是变量，那就反复扫描Subst。
比如一个Subst
x0 = 1
x1 = x0
我们要在其中查找x1。
第一遍扫描发现，x1对应x0。
因为追踪到的还是一个变量，因此再扫描一遍，这时发现x0对应1，是一个普通的值，则返回1。
如果其中某一遍扫描完了，追踪到的还是变量；甚至要找的是一个新的变量，第一遍就没追踪到任何值。这时就直接返回一个包含变量的值。
然后是逻辑编程里面很重要的一个操作unify——合一。
合一是在已有的一个Subst，也就是一组绑定关系上，再新增加一条绑定关系。
比如现有的约束：
x 会 唱和跳
y 会 篮球和rap
如果这时去执行walk操作，查询x或者y会什么。只能得到上面两条分离的信息。
如果在其上执行一个合一操作，指明x和y是同一个人。即变成：
x 会 唱和跳
y 会 篮球和rap
x = y
这时再去执行walk操作，不管是对x还是y执行。都会得到他会唱，跳，rap和篮球。
实现上只要分情况处理即可，当然过程中可能要扩充Subst。
就像前面的例子，就增加了一条绑定关系。
但是如果原有的Subst已经可以推导出x = y，则不会修改Subst了。
这里有一个要注意的点是原始实现里面有对pair的递归处理。这是因为scheme里没有数据结构，只有pair。我的实现里为了简单，没有实现任何的数据结构，所以这里就不需要了。将来如果要支持逻辑编程层面的数据结构，则需要在这里添加相应的处理。
然后是State，其包含一个Subst，即一组绑定关系和一个变量的计数器。
我们前面说过，变量是用一个序号来关联的。
我们当然可以自己手工来分配变量的序号，但这就相当于上层语言里面只有静态的全局变量。没办法在逻辑程序内新增变量，也不方便复用变量（指定两个变量是同一个变量）。
这里的计数器有点像是一个变量分配器。
State其实就是一个解，更精确的说，经过充分简化的State就是一个解。
比如最开始的那个方程组的例子：
x0 = 1
x1 = x0
如果我们从一个空的State开始，将上面两条绑定关系，逐条通过unify操作作用于空的State上。
最终就得到一个解的State
x0 = 1
x1 = 1
因为第二条绑定关系加入的时候，在unify里会先对x1和x0进行walk操作。
这时就知道x0是1了，所以unify添加的绑定关系直接就是x1 = 1。
Stream其实就是一组State。原因就是前面说的，解可能有多组。
当然原始实现里，Stream是一个惰性求值的列表。
这个是为了应对解有无限多组的情况，比如一些不定方程。最经典的就是勾股定理a*a + b*b = c*c。
最后一个概念是Goal。
它是一个函数，参数是一个State，返回值是一个Stream。
最简单的例子就是等价关系，即原始实现中的==，我的实现里叫same。
其实现直接就是应用unify，增加一个绑定关系，然后输出满足绑定关系的解。
这里有个需要注意的点，其实等价关系的返回只有一个State。但是我们还是把它强行封装成了一个Stream。
我理解这是为了统一类型，方便有更好的组合性。因为microKanren作为一个Core语言，只提供最最基本的操作，更多有用的操作需要靠这些基本操作组合。
disj和conj其实就是or和and，是两个高阶函数。用来组合两个Goal，形成一个更大的Goal。
在不考虑无限多组解和惰性求值的情况下，实现还是比较简单的。
这里有两个辅助函数，mplus和bind。其作用分别是将两个Stream拼接起来；将第二个Goal作用到第一个Goal返回的Stream中的每个State上。这也分别就是disj和conj的实现。
最后一个是call/fresh，这个有点像是lisp里的lambda，用来定义函数。这个函数的参数是一个变量，返回值是一个使用了参数中变量的Goal。可以方便的在上层逻辑编程语言的代码里引入变量。
我的实现中这些基本的操作都已经实现。
但是受限于Rust的生命周期检查，无法利用Goal的递归调用来产生无限多组解和惰性求值。
还有一些辅助函数，用来实现更复杂的例子，我都没有做。
如果有兴趣，可以参考原始实现去尝试一下。
接下来我会去学习如何在其中增加linear logic的支持。参见代码仓库。