什么是Datalog
datalog是一种用于描述形如：
u ⇐ p ∧ q ∧ … ∧ t
的逻辑关系的一种一阶逻辑的声明式查询语言。这种形式的逻辑表达式也被称为Horn Clause。读作：谓词u成立，如果条件p ∧ q ∧ … ∧ t成立。
使用Datalog我们可以比较清晰的表达一些 基于传递闭包的表达式， 比如图。
.decl edge(x:number, y:number)
.decl path(x:number, y:number)
.output
edge(1,2).
edge(2,3).
edge(3,4).
path(x, y) :- edge(x, y).
path(x, y) :- path(x, z), edge(z, y).
其中:-就是⇐, ,就是∧。edge关系是我们程序的输入，也被称为facts。
path(1,4)就可以输出所有1到4之间的路径。
基本的语法就这么简单。 当然大多数的datalog实现都会加入，
之类的逻辑符号， 当然这其中特别是not和一般理解上的not式不一样。 具体的可以参考Alice书，其中详细介绍了分层取反和普通的取反有什么的区别。 我后面应该也会开一些文章讲这个。 目前我们自己的datalog实现中也正在实现相关的部分。
为什么使用Datalog
因为研究的原因, 我也开始接触一些logic programming 和datalog。Datalog 从分类上来说是属于prolog的一个子集，相当于在prolog上增加了一些限制。这些限制也使得整个语言不再是图灵完备的， 它只能用于描述能够在P时间内停机的问题。但是这种限制也在有一些领域内确能够着实帮上不少忙， 省去了一些证明的功夫。比如数据库，程序分析，条件约束求解。 因为他的规则上有比较多的限制，实际上datalog engine 的实现可以做到速度极其的快, (配合一些高效的数据结构)。 目前主流的datalog engine是logicblox和souffle。当然你可以使用Z3和其他的条件约束求解器去实现相似的效果，但是从benchmark上看差距巨大。
在程序分析的算法中(特别是采用constrain 描述的时候)， 很多的时候我们都是对一些句法结构的幂集进行操作， 并且计算他的不动点， 这些算法一定都是能够停机。 而Datalog语言的特点正好能够比较好的适应这一点。目前的程序分析框架也有一些选择了使用Datalog比如Doop。
Datalog的输入Facts
因为最早Datalog是一种给数据库设计的查询语言，所以他写的时候很多思路也是和数据库一样的，比如一个lambda表达式我们必须想象成每一个组成部分是数据库中的一张表。然后可以用如下的方式来把这个lambda表达式描述成一个Fact。作为我们datalog程序的输入。
.decl formalArg(id: number, name: symbol)
.decl var(id: number, name: symbol)
.decl abstraction(id: number, arg: number, body: number)
var(1, "x").
formalArg(0, "x").
abstraction(2, 0, 1).
在最上层的语法结构lambda abstraction当中我们可以近似的看作arg和body都是两个外键，他们连向两个属于其他relation表。 这就相当于把原本结构化的AST给彻底flatten了。
我们在从AST生成facts的时候也要非常小心这一点。
一种更加理想的输入
flatten的facts很难阅读，同时也不符合AST的直觉。flatten还有一个很大的问题是在于不容易肉眼去看出一些type问题没比如上面的程序中，abstraction(2, 1, 0).依然可以是一个合法的输入，只是可能在后面的计算中推不出有意义的Facts, 但是毕竟人脑不是数据库。。。直接看就很难受。在程序分析中我们会大量的和IR的AST打交道， flatten style会让我们的处理变得不那么直观。在看doop的实现过程中我也感受到了这一点。 一种更加理想的输入facts应当至少是如下的。 使用s-expression来表达AST是一种比较舒服的方式。
(app (lambda (arg "x") (app (var "x") (var "x")))
(lambda (arg "y") (app (var "y") (var "y"))))
然而目前的Datalog Engine 并没有支持这样的，我的导师和我们团队正在设计的slog会支持这种方式。在slog中我们可以更加舒服的去实现对facts的操作，比如如下是求值的relation。 我觉得会比souffle等其他的主流datalog实现要来的好一些。
;; calculate value
(eval ?(var x) (var x))
(eval ?(lambda x body) (lambda x body))
[(eval ?(app (lambda (arg x) body)
ar)
body-p-val)
<--
(eval ar ar-val)
(subst x ar-val body body-p)
(eval body-p body-p-val)]
[(eval ?(app fn ar) (app fn-val ar-val))
<--
(eval fn fn-val)
(eval ar ar-val)]
