Datalog = Data + Logic，是声明式编程语言(Declarative Programming Language) Prolog的一个子集
Datalog最早作为数据库的查询语言出现，是非图灵完备的编程语言
语法
和数理逻辑的命题逻辑、谓词逻辑基本是一致的，如果看的教材和我一样是Mathematical Logic in Computer Science的话甚至会发现很多描述的语句都是一样的
,表示and
;表示or
!表示not，这些运算可以用括号改变优先级
每条语句的最后要加.表示结束，这个老是忘....
Predicate
即谓词。谓词可以看成是一个函数，n元谓词就是一个(D^nmapsto left{;0,1; ight})的函数，其中(D)是命题变元(变量)与命题常元(常量)构成的集合
在Datalog中，我们讨论的都是有限论域，因此使谓词P为真的命题有限。记(F(P))为所有在谓词P下为真的n元组，则我们称这些元素为Facts。这样就把一个函数变成判断元素是否属于某集合的问题了。
谓词分为两类，算术谓词x >= y和关系谓词Friends(x, y)，算术谓词是Unbounded的
Inference Rules
即推理规则。用PPT的例子就是Datalog的推理规则形如
Adult(x) <- Person(x, age), age >= 18.
<-可以看成是向左的箭头(好形象！)，箭头左侧的称为Head，右侧是Body。语句的意思是"若Body为真，则Head为真"
这句话的意思是"若x是age岁的人 且 age>=18 那么x是成年人"
考虑形式化命题会怎么说
$((forall x)(Person(x)wedge Age(x)>=18))vdash Adult(x) $
观察区别即可发现，如果不使用函数的概念(形式化命题里的(Age()))，我们就需要维护某个元素所有相关的信息，即用元组
求解
就是列真值表，(prodlimits_{Bin Body} |B|)枚举所有可能的值求解(F(P))
Safe Rules
既然涉及到枚举，就要看看是不是可穷尽的
考虑如下两组Rules
A(x) <- B(y), x >= y.
A(x) <- B(y), !C(x, y).
对于1. 如果我们讨论的是正整数域，且(F(B))非空，则必然存在无穷多的x满足要求...
对于2. 由于(F(C))有限，因此(F(!C))有无穷多元素，因此也存在无穷多的x满足要求...
基于上述情况，Datalog对Rules作出了规定：
Head中的变元必须在Body中的某个非否定谓词中出现过(即必须是Bounded Variable)
同样，再考虑如下Rule
A(x) <- !A(x).
很显然就不是合理的Rule，毕竟都不是重言式...因此设定Rules的时候也要考虑是否永真的问题(不能有矛盾)
IDB & EDB
IDB = Intensional DataBase 内涵谓词
EDB = Extensional DataBase 外延谓词
大概理解就是在初始阶段会规定一些谓词，这些就是EDB
而在推理过程中出现的谓词则是IDB。Head一定是IDB，而Body可以IDB、EDB
通常EDB是不可变的(常元)，而IDB可以随着程序的进行而修改，例如如果我想表示"喜欢猫 或 喜欢狗 的人是好人"，那么我可以写
Good(x) <- Likes(x, "Dog").
Good(x) <- Likes(x, "Cat").
当然也可以写
Good(x) <- Likes(x, "Dog"); Likes(x, "Cat").
递归
Datalog的强大之处就在于递归
考虑给定等价关系集合的传递闭包，就可以这么写
Eq(x, y) <- Rel(x, y)
Eq(x, y) <- Eq(x, z), Rel(z, y)
其中Rel(x, y)是EDB中提前定义好的常元
在指针分析中的应用
应用Datalog就能很容易翻译和实现前面讲到的Flow Insensitive & Context Insensitive分析
首先规定下面几个谓词
New(x, o)
Assign(x, y)
Store(x, f, y)
Load(x, y, f)
VCall(l, x, k) #l: x.k(a1,a2...an)
Dispatch(o, k, m)
ThisVar(m, this)
Argument(l, i, ai) #ith argument at l: is ai
Parameter(m, i, pi) #ith parameter at method m is pi
MethodReturn(m, ret) #return var at method m is ret
CallReturn(l, r) #r receives return value at l:
推导规则就是翻译PPT
VarPointsTo(x, o) <- New(x, o).
VarPointsTo(x, o) <- VarPointsTo(y, o), Assign(x, y).
FieldPointsTo(o1, f, o2) <- VarPointsTo(x, o1), VarPointsTo(y, o2), Store(x, f, y).
VarPointsTo(x, o2) <- VarPointsTo(y, o1), FieldPointsTo(o1, f, o2), Load(x, y, f).
CallGraph(l, m), Reachable(m), VarPointsTo(this, o) <- VCall(l, x, k), VarPointsTo(x, o), Dispatch(o, k, m), ThisVar(m, this).
VarPointsTo(pi, o) <- CallGraph(l, m), Argument(l, i, ai), Parameter(m, i, pi), VarPointsTo(ai, o).
VarPointsTo(r, o) <- MethodReturn(m, ret), CallGraph(l, m), CallReturn(l, r), VarPointsTo(ret, o).
全程序分析还要加上一个默认的入口方法，没了