Motivation
Imperative vs Declarative（命令式与声明式）
目标：从人群中选择成年人
Declarative//声明式：该做什么（〜规格）
指针分析，声明式实现（通过Datalog）
•简洁<br>•可读（基于逻辑的规范）<br>•易于实施
Introduction to Datalog
Datalog
Datalog是一种声明性逻辑编程语言，是Prolog的子集。
它作为一种数据库语言出现（1980年代中期）
现在它有各种各样的应用
•程序分析<br>•声明式网络<br>• 大数据<br>• 云计算<br>•…
•无副作用<br>•无控制流<br>•无函数<br>•图灵不完整
Predicates (Data)//谓词（数据）
在数据记录中，谓词（关系）是一组语句
本质上，谓词是数据表
一个事实（fact）断言一个特定的元组（一行）属于一个关系（一个表），即它表示谓词对于特定的值组合为true。
Atoms（原子）
Terms（条目）
Variables（变量）：代表任何值
Constants（常数）
Atoms (Cont.)//原子（续）
P（X1，X2，…，Xn）被称为关系原子（relational atom）
当谓词P包含由X1，X2，…，Xn描述的元组时，P（X1，X2，…，Xn）计算为true。
除了关系原子之外，Datalog还具有算术原子（arithmetic atoms）
Datalog Rules (Logic)//Datalog规则（逻辑）
规则是表达逻辑推理的一种方式
规则还用于指定如何推论事实
Datalog Rules (Cont.)//Datalog规则（续）
“，”可以读为（逻辑and），即对于主体B1，B2，…，Bn，如果所有子目标B1，B2，...和Bn均为true，则为true。
例如，我们可以通过Datalog规则推导出成年人：
如何解释规则？
考虑子目标中变量值的所有可能组合。
如果组合使所有子目标为真，则头部原子（具有相应的值）也为真。
头谓词由所有真实原子组成。
规则解释的一个例子
Datalog program = Facts + Rules
EDB和IDB谓词
按照惯例，Datalog中的谓词分为两种：
EDB (extensional database)//扩展数据库
•先验中定义的谓词<br>•关系是一成不变的<br>•可以看作是输入关系
IDB (intensional database)
•仅由规则建立的谓词<br>•关系是由规则推断的<br>•可以看作是输出关系
Logical Or（逻辑或）
“;”的优先级 （或）小于“，”（和），因此析取可以用括号括起来，例如H <-A，（B; C）。
Negation（否定）
在Datalog规则中，子目标可以是否定的原子，这会否定其含义。
否定的子目标写为！B（…），读为非B（…）
例如，要计算需要参加补考的学生，我们可以编写
Student存储所有学生的位置，PassedStd存储通过考试的学生的位置。
Recursion（递归）
Datalog支持递归规则，该规则允许从其自身（直接/间接）推导IDB谓词。
例如，我们可以使用递归规则来计算图的可达性信息（即，传递闭合）：
其中Edge（a，b）表示图具有从节点a到节点b的边，而Reach（a，b）表示b是从a可达的。
没有递归，Datalog只能表达基本关系代数的查询。
基本上是带有SELECT-FROM-WHERE的SQL
通过递归，Datalog变得更加强大，并且能够表达复杂的程序分析，例如指向分析。
规则安全
对于这两个规则，x的无穷大值都可以满足该规则，这使得A为无穷关系。
•如果每个变量都出现在至少一个非负相关原子中，则规则是安全的。<br>•以上两个规则是不安全的。<br>•在Datalog中，仅允许使用安全规则。
Recursion and Negation
该规则是矛盾的，没有道理。
在Datalog中，原子的递归和负数必须分开。 否则，规则可能包含矛盾，并且推论无法收敛。
执行Datalog程序
Datalog引擎根据给定的规则和EDB谓词推论事实，直到无法推论出新事实为止。
一些现代的Datalog引擎
LogicBlox, Soufflé, XSB, Datomic, Flora-2, …
终止
Datalog程序总是终止，因为：
1）数据记录是单调的<br>2）IDB谓词的可能值是有限的（规则安全性）
Pointer Analysis via Datalog
Pointer Analysis via Datalog
Taint Analysis via Datalog
