Datalog に入門する

とある論文がデータのスキーマ変換を行うために Datalog を用いていた。Prolog は触ったことあるし、Datalog って言葉も聞いたことはあったが、具体的にどんな言語で何が嬉しいのか知らなかったのでちょっと調べてみた。
ついでに Datalog のインプリタとして Soufflé という処理系も触ってみた。

Datalog とは

  • Datalog は、論理型プログラミング言語である Prolog のサブセットであり、主に演繹データベースのクエリ言語として用いられる。クエリは論理的な制約として記述され、その制約を満たすデータをデータベースから抽出する。最近では Datomic のような分散データベースのクエリ言語としても用いられている。
  • Datalog として標準化された言語が言語仕様があるわけではなく、処理系によって構文が異なっていたり、独自の拡張がされていたりする。たとえば、集約関数をサポートするものなどがある。
  • 一般に Datalog の表現力は Prolog より制限されたものであり、チューリング完全ではない。この制限がクエリの効率的な実行(推論)を実現している。また、Datalog は完全に宣言的な言語であるといえる。つまり、記述された命令の順序に意味はない。
  • Datalog を用いたクエリは first-order logic を用いて記述される。また、Datalog のプログラムを構成する要素として extensional predicate (事実の集合、facts と呼ばれる) と intensional predicate (事実から事実を導くルール, rules と呼ばれる) がある。
    • たとえば、データベースの中身は facts であり、抽出したいデータの集合も facts である。このときクエリは rules として記述され、データベースの facts から抽出したいデータの fatcs を導出するものであるといえる。

Datalog - Wikipedia

ここまでのメモ。

  • facts から facts へ変換するルールを rules として記述するだけなので、データベースへの問い合わせだけでなく、異なるスキーマをもつデータ間の変換の操作を Datalog を用いて表現できる。これが Datalog がさまざまなドメインで利用されている背景と言えそう。

Soufflé とは

Datalog の雰囲気が分かったところで、具体的な処理系である Soufflé を触ってみる。公式サイトは以下。

Soufflé は、もともとは Oracle Labs でプログラムの静的解析用に開発されたツールであるが、今ではデータ分析などさまざまな領域において利用されている。ソースコードGithub 上で公開されており、2020年現在もメンテナンスが行われている。ひとつの特徴として、Datalog プログラムを C++ へのトランスパイルが可能であることが挙げられる。これによって、マルチコアなど最新の計算資源を活用したプログラムを書けるのが強みである。

Soufflé のインストール

インストール手順は公式ページにある通り。

Install Soufflé | Soufflé • A Datalog Synthesis Tool for Static Analysis

使っている OS が Ubuntu 20.04.1 LTS (Focal Fossa) なので、apt のためのリポジトリの指定時に bionic の代わりに focal を指定した。

Datalog プログラムの例

以下の公式ページに載っている Datalog プログラムの例を見てみる。
なお本記事に記載するすべてのソースコードは公式ページからの引用である。

Examples | Soufflé • A Datalog Synthesis Tool for Static Analysis

今回のプログラムは、手続き型言語のポインタ解析を行うシンプルな例である。具体的には、変数のフィールドやエイリアスは考慮するが、制御フローは考慮していない。ちゃんと言うと field-sensitive かつ flow-insensitive な Points-to analysis になっている。

ソースコードを上から順に見てゆく。
今回の解析対象の手続き型のプログラムの構造は以下である。

// Encoded code fragment:
//
//  v1 = h1();
//  v2 = h2();
//  v1 = v2;
//  v3 = h3();
//  v1.f = v3;
//  v4 = v1.f;
//

変数として v1, v2, v3, v4 の4つ、オブジェクトとして h1, h2, h3 の3つがある。このポインタ解析では各変数が指しうるオブジェクトの集合を求める。答えから言ってしまうと、今回のポインタ解析では 変数 v1 はオブジェクト h1 または h2 を指し、v2h2, v3h3, v4h3 を指しうる、という結果になる。
ちなみに、本当は変数 v1h2 しか指さないのだが、制御フローを考慮していないので、h1 を指しうると誤検知している。静的解析は安全側に倒す(つまり真の解より広めの範囲を返す)のが一般的であるためこういうことになっている。

次に独自の型を定義している。symbol というのは文字列型だと思っていればよさそう。変数 var、オブジェクト obj、フィールド field がそれぞれ文字列により一意に定められるということ。

.type var <: symbol
.type obj <: symbol
.type field <: symbol

ここから facts を与えてゆく。
まずは4つの関係 (relation) を定義する。このような "関係" という考え方は Prolog と同様であり、データ間に成り立つ事実であると思えばよい。たとえば、assign( a:var, b:var ) は「変数 a が、変数 b の指すオブジェクトを指す」という ab の2項関係である。

// -- inputs --
.decl assign( a:var, b:var )
.decl new( v:var, o:obj )
.decl ld( a:var, b:var, f:field )
.decl st( a:var, f:field, b:var )

そして facts を具体的に与えてゆく。与える facts は解析対象のプログラムに対応している。たとえば、プログラム中で変数 v2v1 に代入されているので、assign("v1","v2") が与えられる。

// -- facts --
assign("v1","v2").

new("v1","h1").
new("v2","h2").
new("v3","h3").

st("v1","f","v3").
ld("v4","v1","f").

ここから最終的に求めたいポインタ解析の結果を導くための rules を定義してゆく。
以下は、エイリアス関係を表現するための alias( a:var, b:var ) である。

// -- analysis --
.decl alias( a:var, b:var ) 
alias(X,X) :- assign(X,_).
alias(X,X) :- assign(_,X).
alias(X,Y) :- assign(X,Y).
alias(X,Y) :- ld(X,A,F), alias(A,B), st(B,F,Y).

変数 abエイリアスの関係にあるのは、4通りのパターンがあることが分かる。
1つ目の alias(X,X) :- assign(X,_). という rule であるが、これは「代入文の左辺に登場する変数はその変数自身とエイリアスの関係にある」という当たり前のケースである。2つ目のケースも同様である。
3つ目の alias(X,Y) :- assign(X,Y). では「代入文があれば左辺の変数は右辺の変数のエイリアスになる」という rule である。
4つ目の alias(X,Y) :- ld(X,A,F), alias(A,B), st(B,F,Y). がやや複雑なケースであり、変数 A, Bエイリアスであり、X = A.FB.F = Y という代入があるとき、変数 X, Yエイリアスになるという rule である。

最後に、ポインタ解析の結果となる pointsTo( a:var, o:obj ) という関係を定義する。

.decl pointsTo( a:var, o:obj )
.output pointsTo
pointsTo(X,Y) :- new(X,Y).
pointsTo(X,Y) :- alias(X,Z), pointsTo(Z,Y).

この rules はシンプルであり、new した場合と、エイリアスの変数が指しうるオブジェクトを自身も指しうる場合の2つからなる。
この関係が最終的に求めたいものであるので、.output pointsTo という命令を書くことで pointsTo.csv というファイルに結果が出力される。以下がその例である。各行が fact になっており、変数とそれが指しうるオブジェクトを意味している。

$ cat pointsTo.csv 
v1      h1
v1      h2
v2      h2
v3      h3
v4      h3

このポインタ解析の例では、「どうやって指しうるポインタを求めるか?」というアルゴリズム的な視点が不要であり「どんな関係が成り立つか?」を定義するだけでよい。これが Datalog のような論理型のプログラミング言語の利点である。実際、この程度のポインタ解析でも非論理型のプログラミング言語で実装するのはけっこうめんどくさい。

その他 Soufflé について

上記は簡単な例であったが、チュートリアル を進めていくと Soufflé のより高度な機能について知ることができた。あとは何か実装したくなったら調べながらやればよさそう。以下は Soufflé に関するメモ。

  • 入出力となる facts はcsv だけでなく SQLite3 データベースにも対応している。つまり、RDB に対するクエリとして使用したり、結果を RDB のテーブルとして格納できる。これは便利そう。
  • チュートリアルの中に、集合 A の要素の順序関係を示す Succ(x:symbol, y:symbol) という関係があったが、これを使って順序の先頭 First(x: symbol) を表現するのに悩んだ。答えは First(x) :- A(x), ! Succ(_, x). である。\{ x \mid x \in A \land \nexists y \in A. \text{Succ}(y, x) \} を求めればよいと思ったが、これを \{ x \mid x \in A \land \forall y \in A. !\text{Succ}(y, x) \} と変形して、y の部分を Datalog の _ で置換するのが正しい。このあたりは Prolog らしい部分であり、慣れが必要そう。
  • Prolog のクエリとしてよくある ?:-parnt(X, Y) みたいな形式は Soufflé ではサポートされてないっぽい。インタラクティブな使い方より、ファイルを入出力とするバッチ処理的な用途が想定されていそう。

所感

  • データ統合やデータ交換などのデータ活用の文脈では、スキーママッピングと呼ばれる、あるデータスキーマを別のスキーママッピングするような操作は重要である。このマッピングの方法にはいろいろあるが、わりと表現力の高いクラスとして GLAV というものがあり、これが Datalog の表現力と近いらしい。これが今後 Datalog の重要性が高まってゆくであろうという理由のひとつである。
  • 一方で、SQL と比較するとやはりクエリを書くのが難しい。クエリの実行時の性能が想定よりも悪いとき、チューニングするのも至難の業だと思われる。人類には早すぎる。