Souffle 学习笔记

前言

Datalog 是一种由 Prolog 分化而来的逻辑编程语言，相比 Prolog 最大的不同在于 Datalog 对于语法做出了很多限制因此是非图灵完全的，然而 Datalog 仍然在数据库和程序分析中有着广泛的应用。Souffle 是 Datalog 的高效实现之一，之前在北大熊英飞老师的公开课上曾经见过但是那个时候不理解也不太会写，最近修程序分析的时候又一次遇到，大作业被迫写了一千多行，因此本文就是用来记录一下 Souffle 编程的经验。

本文的代码可以在 Souffle 的在线编译器中运行。

For English version of this post, see this.

图可达性求解

和一般的命令式语言不同，在 Souffle 中主要的编程对象是“关系”。简单来说，程序员给定输入和输入之间的关系以及规则，之后 Souffle 会根据关系自动推导出输出结果，下面用一个例子来说明。

.decl edge(n: symbol, m: symbol)
edge("a", "b").
edge("b", "c").
edge("c", "d").
.decl reachable (n: symbol, m: symbol)
.output reachable
reachable(x, y):- edge(x, y).
reachable(x, z):- edge(x, y), reachable(y, z).

这个程序会输出一个有向图里每个节点所有可达的节点，接下来逐行分析。

1	.decl edge(n: symbol, m: symbol)

在 Souffle 中 .decl 表示声明一个关系，Souffle 支持 symbol 和 number 作为数据类型，其中 symbol 其实就是字符串类型。

1
2
3

edge("a", "b").
edge("b", "c").
edge("c", "d").

这三行表示对于 edge 这个关系，有三个关系是已知的，这些已知的关系也叫作 facts。

1 2	.decl reachable (n: symbol, m: symbol) .output reachable

这一行声明了一个新关系 reachable，并且用 .output 来输出这个关系。

1 2	reachable(x, y):- edge(x, y). reachable(x, z):- edge(x, y), reachable(y, z).

这两行就是定义关系的规则了，他定义了两件事：

如果 x 和 y 之间存在一条边，那么 x 可以到达 y
如果 x 和 y 存在一条边，并且 y 可达 z，那么 x 可以到达 z

看起来非常的符合直觉，但是为了进一步理解 Souffle 的原理，这里要强调两个隐藏语义：

:- 右边的变量如果出现在左边那么具有“任意”的语义，比如第一行中的 x 和 y 表示的任意 x 和 y
:- 右边的变量如果没有出现在左边，那么具有“存在”的语义，比如第二行右边的 y

结合这两点，其实第二行的含义具体说应该是：对于 reachable 关系中任意的 x 和 z ，如果存在一个y，满足 x 和 y 之间有一条边并且 y 可达 z，那么 x 可达 z，即满足 reachable。

这样理解的话虽然看起来是更复杂了，但是可以帮助接下来理解 Souffle 是如何求解这个问题的。

原理

为了更好的编写 Souffle 程序，现在一个很重要的问题是 Souffle 怎么实现求解上述程序的？注意 edge 和 reachable 的实际含义都是我们人为加上去的，在 Souffle 眼里只有关系和规则而已。为了解答这个问题，需要引入不动点的概念，简单来说就是给定一个集合 S 和一个作用域和值域都是集合的规则 g 有：

\[ S = g(S) \]

那么 S 就是一个不动点。

Souffle 实际上求解的过程就是根据已有的 facts 不断的应用所有定义的规则，直到所有集合达到 不动点，以上述图可达性的例子来说明：

edge 关系没有定义规则，因此 edge 的不动点集合就是所有的 facts，即 (a, b), (b, c), (c, d)
反复应用 reachable 第一条规则，可以把 edge 关系中所有的 facts 添加到 reachable 中，即 (a, b), (b, c), (c, d)
应用 reachable 第二条规则，注意之前对这条规则的解释，可以添加几个新的 facts 到 reachable 中，即 (a, c), (a, d), (b, d)，此时 reachable 关系的集合为 (a, b), (b, c), (c, d), (a, c), (a, d), (b, d)
反复应用源代码中所有的规则，所有集合不再变化，程序结束。

局限

不动点算法可以在很多场景下用 Souffle 写出非常符合直觉漂亮的代码，但是相应的其也有局限性：

上面解释不动点算法的时候有一个很强的假设，那就是g必须是（非严格）单调递增的，放在 Souffle 里就意味着如果规则如果存在环形依赖，那么这个环里不能出现否定，这样才能保证所有的规则是单递增的。也就是说，下面的程序 Souffle 无法求解

.decl p(x: number)
.decl q(x: number)

p(x) :- !q(x).
q(x) :- !p(x).

此外，为了能表达更复杂的语义，比如一对多的关系，Souffle 提供了一部分复杂数据结构比如链表的支持：

.type IntList = [next: IntList, x: number]
.decl L(l: IntList)
L([nil,10]).
L([r1,x+10]) :- L(r1), r1=[r2,x], x < 30.
.decl Flatten(x: number)
Flatten(x) :- L([_,x]).
.output Flatten
.output L

然而相比常见的命令式语言，无论是声明还是使用上显然都不太方便。

最后，除了链表这样复杂的程序结构，我发现还有一类关系是 Souffle 比较难以表达的，那就是元素聚集相关的逻辑，比如假设我们定义“如果一个店铺卖的苹果价格全部小于25，那么这样的店铺我们称之为便宜店铺”，并且给定 facts：

.decl apple(price: number, shop: number)

apple(10, 1).
apple(23, 2).
apple(32, 2).

.decl cheapApple(price: number, shop: number)

cheapApple(price, number) :-
    apple(price, number), price <= 25.

// A cheap shop only sells apples cheaper than 25
// and thus only shop 1 meets this requirement.
.decl cheapShop(shop: number)

直觉上可能会写出：

1	cheapShop(shop) :- apple(x, shop), x < 25.

但是很不幸这是不对的，因为其中 x 具有存在语义，所以店铺 2 也会被算在其中。确切来说在这种情况下，很难找到一种合适的方式表达“某个店铺中任意苹果的语义”，因此只能用count来曲线实现：

.decl cheapCount(shop: number, cnt: number)

cheapCount(shop, cnt) :-
    apple(price, shop),
    count : { cheapApple(_, shop) } = cnt.

.decl appleCount(shop: number, cnt: number)

appleCount(shop, cnt) :-
    apple(price, shop),
    count : {apple(_, shop)} = cnt.

cheapShop(shop) :-
    appleCount(shop, cnt),
    cheapCount(shop, cnt2),
    cnt = cnt2.

.output cheapShop

然而 count 也并不是万能的，因为很容易写出 witness 问题，这里不做展开了。

UPDATE(2023/02/19)：正确方法不是 count，是先对要证明的 property 取反把存在语义变成任意语义然后再用 Souffle 编程解答。

后记

Souffle 是一门非常有趣的语言，而且在写文的这个时间点仍然在积极开发，性能也非常不错，然而我最后作业还是选择了用 Python 实现，原因主要就是上面提到几点局限性，不过 Souffle 整体编写体验还是很不错的，在很多地方都符合直觉，希望发展的越来越好。

澪同学的博客 - 个人的技术分享

Souffle 学习笔记

前言

图可达性求解

原理

局限

后记

参考资料