datalog学习

Datalog 是一种（声明式）基于逻辑的查询语言，允许用户执行递归查询。类型系统是静态的

Souffle安装

ubuntu :

sudo wget https://souffle-lang.github.io/ppa/souffle-key.public -O /usr/share/keyrings/souffle-archive-keyring.gpg
​
echo "deb [signed-by=/usr/share/keyrings/souffle-archive-keyring.gpg] https://souffle-lang.github.io/ppa/ubuntu/ stable main" | sudo tee /etc/apt/sources.list.d/souffle.list
​
sudo apt update
​
sudo apt install souffle

a simple example:

example.dl:

// example.dl
​
// 声明，edge是关系，可以理解为一阶逻辑里的二元关系
.decl edge(x:number, y:number)
// 没有指定文件，默认从 edge.facts 中读取
.input edge
​
//声明，path也可以理解成二元关系
.decl path(x:number, y:number)
// 输出为 path.csv
.output path
​
//这就是一般的 H if B1 B2 B3的形式，表示(B1 B2 B3)蕴含H
//这里是如果存在边x到有的边，那么就存在x到y的路径。
//即满足于关系path(x,y)，当且仅当满足edge(x, y)或者path(x, z), edge(z, y)
//注意定义联系的时候都会有点结尾。
path(x, y) :- edge(x, y).
path(x, y) :- path(x, z), edge(z, y).

edge.facts:

1   2
2   3

执行命令：

souffle -F. -D. example.dl
# souffle -F./input -D./output example.dl

自动输出：path.csv

1   2
2   3
1   3

语言特点

1. 原子atom：在 Datalog 语言中，称返回值为 True 或者 False 的 表达式（Expression） 为 原子（Atom） 。

2. P(x1,x2,...,xn)：关系型原子（Relational Atoms） ，其中 P 称为 谓词（Predicates） 或 关系（Relation） ， xi(1≤i≤n) 称为 实参（Arguments） 或者 项（Terms）

   P(x1,x2,...,xn)=True⇔(x1,x2,...,xm)∈P

   此时，称为 (x1,x2,...,xn) 为 P 中的一个 事实（Fact）

3. 规则rules：H←B1,B2,...,Bn

   • H 称为头部（Header），是规则的结果（Consequent），其形式上是一个原子。

   • B1,B2,...,Bn 称为主体（Body），是规则的前提（Antecedent），其中的 Bi 是一个原子或者原子的否定（见10.2.5），称为子目标（Subgoal）。

   , 表示合取 ; 表示析取（，的优先级高于 ;）

   语法糖：可以编写具有多个头的规则：

   B(x), C(x) :- A(x).     // 同时定义

   Horn clause : 如果一个clause最多只导出1个结论，那么这种clause就称为horn clause

   只有body的horn子句，无头部，Query查询：

   :- B1, B2, ..., Bn.

4. EDB与IDB：datalog的两类谓词：

   • EDB是外延数据库（输入关系，关系不可修改）

   • IDB是内涵数据库（输出关系）

   头部只能是IDB，但主体部分的原子既可以是 EDB ，也可以是 IDB 。换句话说， Datalog 支持递归的规则（Recursive Rules）

5. 递归：

   Datalog允许一个IDB是直接或者间接从它本身推出来

   Reach(from, to) <-
       Edge(from, to).
   ​
   Reach(from, to) <-
       Reach(from, node),
       Edge(node, to).

6. 规则安全：

   如果一个规则中的每个变量都在至少一个非否定的关系型原子中出现过，那么这个规则就是安全（Safe）的

   一个原子的递归和否定必须分开，否则这个规则可能会包含矛盾，且逻辑推理无法收敛

7. 不动点：

   Datalog 程序具有单调性，其次规则安全保证了 IDB 的所有可能值是有限的，从而根据单调有界原则， Datalog 程序总能够终止

   解释满足埃尔布朗模型

语法

1. 数据类型

   静态类型系统。只有四类基础类型，symbols 相当于字符串，number 是数字。unsigned 和 float 用的较少。

2. 关系定义：

   关系必须声明后才能使用

   .decl edge(a:symbol, b:symbol)

3. souffle算术表达式

   比如打印斐波那契数列：

   .decl Fib(i:number, a:number)
   .output Fib
   Fib(1, 1).
   Fib(2, 1).
   Fib(i + 1, a + b) :- Fib(i, a), Fib(i-1, b), i < 10.

   一些特别的算术函子：

   • 幂：a ^ b

   • 计数器：autoinc()

   • 位操作：x band y、x bor y、x bxor y 和 bnot x

   • 逻辑运算：x land y、x lor y 和 lnot x

   • autoinc()：

     每次求值都产生一个新数字，可为符号创建唯一编号当标识符，但不允许在递归关系中调用

     .decl A(x: symbol)
     A(“a”). A(“b”). A(“c”). A(“d”).
     
     .decl B(x: symbol, y: number)
     .output B
     B(x, autoinc()) :- A(x).    // 为 a、b、c、d 各生成一个标识符

4. 聚合：

   • 计数：count:{<sub-goal>}

     输出蓝色汽车的数量：

     .decl Car(name: symbol, colour:symbol)
     Car("Audi", "blue").
     Car("VW", "red").
     Car("BMW", "blue").
     
     .decl BlueCarCount(x: number)
     BlueCarCount(c) :- c = count:{Car(_, "blue")}.
     
     .output BlueCarCount

   • 最大值/最小值/求和：max <var>:{<sub-goal(<var>)>} 、 sum <var>:{<sub-goal>(<var>)>}

     .decl A(n:number)
     A(1). A(10). A(100).
     
     .decl MaxA(x: number)
     MaxA(y) :- y = max x:{A(x)}.
     
     .output MaxA

5. Records：

   .type <name> = [ <name_1>: <type_1>, ..., <name_k>: <type_k> ]

   // Pair of numbers
   .type Pair = [a:number, b:number]
   
   .decl A(p: Pair)  // declare a set of pairs
   A([1,2]).
   A([3,4]).
   A([4,5]).
   
   .decl Flatten(a:number, b:number) output
   Flatten(a,b) :- A([a,b]).

6. 组件与实例化：

   .comp：声明组件

   .comp MyComponent {
       .type myType = number        // type
       .decl TheAnswer(x:myType)    // component relation
       TheAnswer(42).               // component fact
   }

   .init：初始化组件

   .init myInstance1 = MyComponent         // 实例化
   
   .decl Test(x:number)
   Test(x) :- myInstance1.TheAnswer(x).    // . 限定
   .output Test

   可以用类型与泛型：

   .comp ParamComponent<myType> {
       .decl TheAnswer(x:myType)    // component relation
       TheAnswer(42).               // component fact
       .output TheAnswer            // component output directive
   }
   .init numberInstance = ParamComponent<number>
   .init floatInstance = ParamComponent<float>

   可以用参数传递决定实例化组件类型：

   .decl R(x:number)
   .comp Case<Selector> {
      .comp One { 
        R(1). 
      } 
      .comp Two { 
        R(2).
      } 
      .init selection = Selector // instantiation depending on type parameter "Selector" 
   } 
   .init myCase = Case<One> 
   .output R

7. 继承 :

   组件 Base1 和 Base2 将所有组件元素传递给子组件 Sub

   .comp Base1 {
       .type myNumber = number
       .decl TheAnswer(x:myNumber)
       TheAnswer(42).
   }
   .comp Base2 { 
       TheAnswer(41). 
   }
   .comp Sub  : Base1, Base2 { // inherit from Base1 and Base2
       .decl WhatIsTheAnswer(n:myNumber)
       WhatIsTheAnswer(n) :- TheAnswer(n).
       .output WhatIsTheAnswer
   }
   .init mySub = Sub

   可以用 .override 进行覆盖：

   .comp Base {
       .decl R(x:number) overridable
       R(1).
       R(x+1) :- R(x), x < 5. 
       .output R
   }
   .comp Sub : Base {
       .override R
       R(2).
       R(x+1) :- R(x), x < 4. 
   }
   .init mySub = Sub

   类型参数化和继承：

   .comp A<T> { .... }
   .comp B<K> : A<K> { ... }

Evaluation

1. bottom-up evaluation strategies

   start with the facts and repeatly apply the rules

   • naive evaluation

     从已知的事实出发，逐一匹配规则，直到不能再生成新的事实为止。这种朴素的求解方式可能会导致重复计算，因为它会对每个规则进行完整的匹配，即使部分匹配已经在之前的推理中得到了。

   • semi-naive evaluation

     引入了一种增量的策略。它在朴素求值的基础上，通过跟踪已经计算过的事实，只对新增的事实进行推理和计算。这样可以避免对已经知道的事实进行重复计算，提高了求解效率

2. top-down evaluation strategies

   TODO

3. magic-set

   a technique used to reduce the number of irrelevant tuples computed

   原：

   a(x,y) :- b(x,z), c(y,z).
   query(x) :- a("foo", x), !g(x).

   现：

   a("foo", y) :- b("foo", z), c(y,z).
   query(x) :- a("foo", x), !g(x).

   To enable the transformation on the full program, use

   souffle --magic-transform=* foo.dl

不带call的指针分析

pt0.dl

.decl New(x:symbol, o:symbol)
.input New

.decl Assign(x:symbol, y:symbol)
.input Assign

.decl Store(x:symbol, f:symbol, y:symbol)
.input Store

.decl Load(y:symbol, x:symbol, f:symbol)
.input Load

.decl VarPointsTo(x:symbol, o:symbol)
.decl FieldPointsTo(oi:symbol, f:symbol, oj:symbol)

// Rules

VarPointsTo(x, o) :-
    New(x, o).

VarPointsTo(x, o) :-
    Assign(x, y),
    VarPointsTo(y, o).

//x.f = y
FieldPointsTo(oi, f, oj) :-
    Store(x, f, y),
    VarPointsTo(x, oi),
    VarPointsTo(y, oj).

//y = x.f
VarPointsTo(y, oj) :-
    Load(y, x, f),
    VarPointsTo(x, oi),
    FieldPointsTo(oi, f, oj).

.output VarPointsTo
.output FieldPointsTo

New.facts

b	o1
c	o3

Load.facts

e	d	f

Assign.facts

a	b
d	c

Store.facts

c	f	a
c	f	d

命令行：

souffle -D. -F. pt0.dl