# Datalog rule の simplification を実装する

## Datalogの構文のおさらい

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

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

1つのrule $A \mathrel{\mathord{:}\mathord{-}} C_1, …, C_n$ に於いて，$A$ を**head**，$C_1, …, C_n$ を**body**と呼ぶ．また，各 $C_i$ を**節**と呼ぶ．

## simplificationの例

加藤先生から頂いた例を挙げる．

### 例 (1)

-tracks(TRACK, DATE, RATING, ALBUM) :-
    albums(ALBUM, _), albums(ALBUM, V6845),
    tracks(TRACK, DATE, RATING, ALBUM), tracks(TRACK, DATE, RATING, ALBUM),
    RATING = 1.

↓ `V6845` は1箇所しか出現していないので `_` に置き換えられる

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

↓ 重複する `albums(ALBUM, _)` と `tracks(TRACK, DATE, RATING, ALBUM)` はそれぞれ1つにできる

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

### 例 (7)

-albums(ALBUM, QUANTITY) :-
    albums(ALBUM, QUANTITY), albums(ALBUM, QUANTITY),
    tracks(_, _, _, ALBUM), tracks(V6853, V6854, V6855, ALBUM), V6855 = 1.

↓ `V6853` と `V6854` はそれぞれ1箇所しか出現していないので `_` に置き換えられる

-albums(ALBUM, QUANTITY) :-
    albums(ALBUM, QUANTITY), albums(ALBUM, QUANTITY),
    tracks(_, _, _, ALBUM), tracks(_, _, V6855, ALBUM), V6855 = 1.

↓ 重複する `albums(ALBUM, QUANTITY)` は1つにできる

↓ `tracks(_, _, _, ALBUM)` は `tracks(_, _, V6855, ALBUM)` より制約として緩いので消せる

-albums(ALBUM, QUANTITY) :-
    albums(ALBUM, QUANTITY), tracks(_, _, V6855, ALBUM), V6855 = 1.

### 例 (17)

-tracks(TRACK, DATE, RATING, ALBUM) :-
    albums(ALBUM, V34), tracks(TRACK, DATE, RATING, ALBUM),
    tracks(V31, V32, V33, ALBUM),
    not albums(ALBUM, _), not albums(ALBUM, V34).

↓ `albums(ALBUM, V34)` と `not albums(ALBUM, V34)` が矛盾するためruleとして不要とわかる

削除

## simplificationの定式化

上記の例をもとに定式化を行なう．

rule集合のsimplificationは，以下の手順のいずれかを有限回適用することによって行なう（1–3は各rule単独に対する操作で，4はrule集合全体に対する操作）：

1. headに出現せず，かつbody中に1箇所しか出現しない変数は，$\_$ で置き換える．等式の変数がそれに該当する場合は，その等式自体を消す．
2. bodyの節に一方が他方よりも**緩い**組がある場合，緩い方を消す．
- 同一の節が複数個ある場合に1つを残して消すという操作も特殊な場合としてこれに含まれる．
3. bodyの節に**互いに矛盾する**節の組がある場合，そのrule自体を消す．
4. 同一のruleがある場合は1つにする．

$A'$ が $A$ よりも（制約として）**緩い**とは，以下で定義される $A ⊢ A'$ が成り立つことを言う（気持ちとしては，$A$ が成り立つならば必ず $A'$ が成り立つ，すなわち $A ⇒ A'$ が言えることに相当する）：

$$
\begin{align*}
\frac{
∀i ∈ \{1, …, n\}. t_i ≽ t'_i
}{
r(t_1, …, t_n) ⊢ r(t'_1, …, t'_n)
}
&
&\frac{}{x ≽ x}
&
&\frac{}{x ≽ \_}
&
&\frac{}{\_ ≽ \_}
\end{align*}
$$

端的に言えば，$A$ の変数の一部を $\_$ に置き換えて $A'$ にできるということである．また，この定義を以下によって節にも拡張する：

$$
\begin{align*}
&\frac{
A ⊢ A'
}{
¬A' ⊢ ¬A
}
&
&\frac{}{x = c ⊢ x = c}
\end{align*}
$$

そして，positiveな節 $A$ とnegativeな節 $¬A'$ が $A ⊢ A'$ を満たすとき，$A$ と $¬A'$ は**互いに矛盾する**という．また，$c ≠ c'$ なる等式制約の組 $x = c$ と $x = c'$ も**互いに矛盾する**という．

## simplificationのアルゴリズム化

上記のsimplificationの書き換えは，実際には以下のようなアルゴリズムで処理できる：

* 1の書き換えを可能なだけやってその後2の書き換えを可能なだけやるという操作をひとかたまりとしてこれを反復し，不動点に達するまで行なう．
* 不動点に達したら，3の判定を行なってbodyに矛盾のあるruleを消す．
* 4により重複を削減する．

1と2で反復が必要なのは，1の結果新たに2が適用できるようになる場合も，2の結果新たに1が適用できるようになる場合もあるため．例えば

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

はまず1の書き換えで `X` が消せて，その後2で `albums(ALBUM, TRACK)` より緩い `albums(ALBUM, _)` を消せるようになる．一方で

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

はまず2の書き換えで重複する `albums(ALBUM, X)` を1つにでき，その後1を適用して `albums(ALBUM, _)` に書き換えられるようになる．

また，この反復に於いては，書き換えが生じた場合には辞書式順序の入った組 (節の個数, 変数の個数) が真に減少し，かつ (0, 0) が最小元なので，必ず不動点に到達する．