# Datalog rule の “インライン展開” による平坦化を実装する

## 概要

下記のいただいた要望に対応し，何を実現するかを定式化する．

> ## 追加項目2:否定を含まないDatalog式の平坦化
>
> BIRDS では得られた Datalog から SQL を出力するが、出力される SQL をできるだけ単純化することで実行時の速度を上げることができる。そのために今回は Datalog 式を平坦化する実装を行う。具体的には、body に出現する positive な idb アトムをその idb アトムを head とする rule の body で置換する。この時、idb アトムの引数が anonymous variableのときも考慮に入れて正しく置換する。

## 定義おさらい

$x$ が変数を，$c$ が定数を，$p$ が述語（delta predicateも含む）をそれぞれ動くメタ変数として，Datalogの**rule**の構文は以下の $R$ で定義される：

$$
\begin{align*}
t &::=\ x\ |\ \_
\\
A &::=\ p(t, …, t)
\\
C &::=\ A\ |\ ¬A\ |\ x = c
\\
𝑪 &::=\ C, …, C
\\
R &::=\ A \mathrel{\mathord{:}\mathord{-}} 𝑪
\end{align*}
$$

1つのrule $(A \mathrel{\mathord{:}\mathord{-}} C_1, …, C_n)$ に於いて，$A$ を**head**，$C_1, …, C_n$ を**body**と呼ぶ．また，各 $C_i$ を**節**と呼ぶ．節のコンマ区切りの列はメタ変数 $𝑪$ で書くことにする．

Datalogのプログラム $D$ は，有限個のruleの集合である．プログラム $D$ と述語 $p$ に対し，$p(t_1, …, t_m) \mathrel{\mathord{:}\mathord{-}} C_1, …, C_n$ の形のruleが $D$ 中に含まれるとき，つまり $p$ がいずれかのruleのheadにくる述語であるとき，$p$ は $D$ に於いて**IDB述語** (*IDB predicate*)であるという．IDBはintensional databaseの略．一方，$p$ が $D$ のruleのbody中には出現するがheadにはこないとき，$p$ は $D$ の**EDB述語** (*EDB predicate*)であるという．EDBはextensional databaseの略．

気持ちとしてはEDB predicate $r$ は “データベースに実際に物理的に格納されているテーブル” に対応する述語で，どちらかといえばこれらを前提としてdelta predicate $+r$ などのIDB predicateに対する更新規則の集まりであるプログラム $D$ を書く，と言った方が実態を反映している．

## 注意すべきこと

**入力されるプログラム $D$に於いては，各述語 $p$ に対し，$D$ 中で $p$ をheadとするruleは一般に1つとは限らない**．複数ある場合は，直観的にはそれらのORである．“インライン展開” に於いてはこれも加味する必要がある．

## 平坦化の例

-tracks(TRACK, DATE, RATING, ALBUM) :-
    tracks(TRACK, DATE, RATING, ALBUM), RATING = 0.
-tracks(TRACK, DATE, RATING, ALBUM) :-
    tracks(TRACK, DATE, RATING, ALBUM), RATING = 1.

+omitted_tracks(T, A) :-
    -tracks(T, _, _, A).

↓ `-tracks` の適用を “インライン展開” する

-tracks(TRACK, DATE, RATING, ALBUM) :-
    tracks(TRACK, DATE, RATING, ALBUM), RATING = 0.
-tracks(TRACK, DATE, RATING, ALBUM) :-
    tracks(TRACK, DATE, RATING, ALBUM), RATING = 1.

+omitted_tracks(T, A) :-
    tracks(T, _, V1, A), V1 = 0.
+omitted_tracks(T, A) :-
    tracks(T, _, V1, A), V1 = 1.

**複数の規則がある述語に関しては，それを定めている各規則ごとにインライン展開して複製するとよい**．最悪の場合ruleの個数が指数的に膨らむが，それはsimplificationで減らすなどの対処ができればよいだろう．

## 平坦化の処理で何をやるか

1. 各 `_` (anonymous variable) に対して1つずつfreshな変数名を生成して置換する．
2. rule集合をもとに，どのIDB述語がどのIDB述語に依存しているかの依存関係を抽出する．より正確には，rule $(p(…) \mathrel{\mathord{:}\mathord{-}} C_1, …, C_n)$ のいずれかの $C_i$ が $p'(…)$ または $¬p'(…)$ であるとき，$p$ は $p'$ に依存しているとする．
- ここで平坦化の変換を目的とする限りは $¬p'(…)$ の出現を無視してもよいのだが，考慮しなかった場合は相互依存を含む不正なプログラムを変換してしまいうる．
3. 2で抽出した依存関係を有向グラフにし，有向閉路がない（つまり相互依存するIDB述語の組がない）ことを確認しながらトポロジカルソートを行なう．
4. 3でソートされてできたIDB述語の列を依存関係が浅い側から見ていき，対応するruleに対して順に以下で述べる “インライン展開” を行なう．
- より正確には，プログラム $D$ のruleたちが依存関係の浅い順に並んだ列 $R_1, R_2, …, R_N$ に対して，プログラム $D_i := ℛ'_1 ∪ … ∪ ℛ'_{i - 1}$ を用いて $R_i$ をインライン展開して $ℛ'_i := \mathrm{inlined}_{D_i}(R_i)$ を得る，という処理を $i ∈ \{1, …, N\}$ に対して（番号の若い側から）繰り返す．最終的に全てのIDB述語の出現がインライン展開されたプログラム $D_N := ℛ'_1 ∪ … ∪ ℛ'_N$ を得る．

rule $R$ に対する，プログラム $D$ を用いたインライン展開結果のrule集合 $\mathrm{inlined}_D(R)$ は以下で定義される：

$$
\begin{multline}
\mathrm{inlined}_D(p(X_1, …, X_m) \mathrel{\mathord{:}\mathord{-}} C_1, …, C_n) :=
\\
\{
p(X_1, …, X_m) \mathrel{\mathord{:}\mathord{-}} 𝑪'_1, …, 𝑪'_n
\mid
𝑪'_1 ∈ \mathrm{inlined}_D(C_1) ∧ … ∧ 𝑪'_n ∈ \mathrm{inlined}_D(C_n)
\}
\end{multline}
$$

ただし，$𝑪'_1, …, 𝑪'_n$ は節の列を連接してできる列を表す．

ここで節 $C$ のインライン展開結果となる節の列の集合 $\mathrm{inlined}_D(C)$ は以下で定義される（複数の節がコンマ区切りで並んだもの）：

$$
\begin{align*}
\mathrm{inlined}_D(x = c) &:=
\{x = c\}
\\
\mathrm{inlined}_D(¬A) &:=
\{¬A\}
\\
\mathrm{inlined}_D(p(X_1, …, X_n)) &:=
\{p(X_1, …, X_n)\}
\\
&\quad\quad\quad(\mathrm{if}\ p\ \mathrm{is\ not\ an\ IDB\ predicate})
\\
\mathrm{inlined}_D(p(X_1, …, X_n)) &:=
\{
[X_1/Y_1, …, X_m/Y_m]𝑪
\mid
(p(Y_1, …, Y_m) \mathrel{\mathord{:}\mathord{-}} 𝑪) ∈ D
\}
\\
&\quad\quad\quad(\mathrm{otherwise})
\end{align*}
$$

negativeな節は置換しないことに注意．

## 実装方針

`inlining.ml` に平坦化処理を追加する：

type error = …

let inline_rules (metadata : metadata) (rules : rule list) : (rule list, error) result = …

`metadata` は各述語のアリティなどの情報を含む何らかのデータ．