# Datalogの形式を復習
## データベーススキーマ，データベースインスタンス，原子式 etc.
**データベーススキーマ** $\mathcal{D}$ とは，リレーション名をその属性名の列へ紐づける有限写像
$$
\{r_1 ↦ (A_{1 1}, …, A_{1 n_1}), …, r_n ↦ (A_{N 1}, …, A_{N n_N})\}
$$
である． $\mathcal{D}$ の **データベース**（または **データベースインスタンス**） $D$ とは，$\mathcal{D}$ の各リレーション名 $r_i$ に対して何らかの $n_i$ 項リレーション $R_i$ を紐づける写像
$$
\{r_1 ↦ R_1, … r_N ↦ R_N\}
$$
である．**原子式** (*atom*, *atomic formula*) とは $r(t_1, …, t_n)$ の形の式をいう（$t$ の形式は何かしら定まっているとする）．いずれの $t_i$ も定数であるような原子式は**基底原子式** (*ground atom*) と呼ばれる．
データベースインスタンスは有限個の基底原子式の集合で表すことができる．
**Datalogプログラム**とは $H \mathrel{\mathord{:}\mathord{-}} L_1, …, L_n$ の形であって $H$ および各 $L_i$ が原子式であるものが有限個集まったもの．このDatalogプログラムに対する**入力**は**外延的データベース** (*extensional database*, *EDB*) と呼ばれる基底原子式の有限集合であり，一方で**出力**は**内包的データベース** (*intensional database*, *IDB*) と呼ばれる．
Datalogプログラムで使われる**述語**は**EDB述語**と**IDB述語**に分かれており，それぞれ原子式としての $r$ はEDBのリレーションとIDBのリレーションに対応する．
Datalogプログラム $P$ の出力をIDBのうちの1つのシンボル $r$ に対応するリレーション $R$ に制限したものを**Datalogクエリ**といい，$(P, R)$ で表す．（疑問： まだ若干わからない．記法としては $(P, r)$ の方が妥当なんじゃなかろうか？）
IDB述語 $r$ が**充足可能** (*satisfiable*) であるとは，或るEDBのデータベースインスタンス $D$ が存在して $P$ に $D$ を入力して得られるIDBの $r$ に対応するリレーション $R$ が非空であることをいう．
## 双方向変換 (BX)
**双方向変換** (*bidirectional transformation*, *BX*) とは，以下を満たす $(get, put)$ をいう：
1. $∀S. put(S, get(S)) = S$
2. $∀S∀V'. get(put(S, V')) = V'$
気持ちとしては $S$ がsource databaseで，$V$ がview．$get$ は “source databaseからviewを得る函数” であり，$put$ は “現在のsource database $S$ と新しいview $V'$ とを受け取って，$V'$ に整合させるように $S$ を更新した新しいsource databaseを返す函数”．1つ目の規則は “viewを更新していなければsource databaseは更新されない” ことを，2つ目の規則は “新しいview $V'$ によって更新されたsource databaseからviewを取り出すと $V'$ に一致する” ことを表す．
```
get
S |--------> V
__ _
\ |
\ | u
\ |
\ v
\
S' <-------| V'
put
```
以下のように，viewの更新 $u$ に対して $T(u)(S) := put(S, u(get(S)))$ なるsource databaseの更新 $T(u)$ が対応すると捉えてもよい：
```
get
S |-------> V
_ _
| |
| T(u) | u
| |
v v
S' V'
```
view update strategy $put$ に対し，或る $get$ が存在して $(get, put)$ がBXであるとき，$put$ は**valid**であるという．
実は $put$ に対して $(get, put)$ がBXであるような $get$ は高々1つしか存在しないことが示されている．
## Datalogによるputの記述方法
source databaseの更新を表現するために，**差分リレーション** (*delta relation*) という仕組みを用いる．これはシンプルなもので，例えば名前 $r$ に対応するリレーション $R := \{(1, 2), (1, 3)\}$ に対して差分リレーション $ΔR := \{-r(1, 2), +r(1, 4)\}$ の適用は $R ⊕ ΔR = \{(1, 4), (1, 3)\}$ である．差分リレーション $ΔR$ が “同一要素の追加と削除を共に含まない” とき，つまり例えば $+r(1, 1)$ と $-r(1, 1)$ を共に含んでいたりしないとき，$ΔR$ は**non-contradictory**であるという．
例として，$\mathcal{D} := \{r_1 ↦ (A), r_2 ↦ (A)\}$ で，インスタンスが $D = \{r_1 ↦ R_1, r_2 ↦ R_2\}$ であり，view $V := R_1 ∪ R_2$ が定められているとする（正確な記述をするならviewの定義もスキーマレベルでないとおかしいが，便宜的にこう書く）．このとき，$V$ に内容を追加する更新をした場合，source databaseの更新としては $R_1$ に追加すべきなのか $R_2$ に追加すべきなのか決定できない曖昧性がある．こうした曖昧性をなくしたDatalogでのputの記述方法が例えば以下：
```
-r_1(X) :- r_1(X), ¬v(X)
-r_2(X) :- r_2(X), ¬v(X)
+r_1(X) :- v(X), ¬r_1(X), ¬r_2(X)
```
`:-` は逆向きの「ならば」に相当し，したがって各行は以下を表す：
1. `r_1` に入っていて更新後のview `v` に入っていない要素があったら，`r_1` からそれを取り除く．
2. `r_2` に入っていて更新後のview `v` に入っていない要素があったら，`r_2` からそれを取り除く．
3. `r_1` と `r_2` に入っておらず，更新後の `v` には入っている要素があったら，それを `r_1` に追加する．
ここでは特に3が曖昧性を排除することに貢献している．上記は要するに $S$ と $V'$ から $S$ に適用すべき差分リレーション $ΔS = putdelta(S, V)$ を求める規則であると言える．こうして $putdelta$ を介して $put(S, V) := S ⊕ putdelta(S, V)$ で $put$ を定義する記述が行なわれている．上記のようなプログラムを**Datalog putback program**と呼ぶ．
Datalog putback program $P$ が，任意の入力 $S$ と $V$ に対してnon-contradictoryな差分リレーション $ΔS$ を返すとき，$P$ は**well-defined**であるという．
# 今回やること
* 参考： [BIRDS 機能拡張案件 2022 07 - HackMD](https://hackmd.io/8IonbopESZG4q1_1cinvlw?view)
> SQL文の生成にこれまでは `state-based` アプローチを取っていたが、実行速度の改善のために `operation-based` なアプローチへ変更したい。
> - Deriving operation-based BX from state-based BX specification
>
> * Δ-predicates for views occurring in body
あーなるほど，「今までは `v(X)` のようにviewの “状態” を述語にしていたが，それを `+v(X)` のような表現で扱うようにしたい」ということだろうか？ したがって，上記の例は以下のように書くことになる？：
```
-r_1(X) :- r_1(X), -v(X)
-r_2(X) :- r_2(X), -v(X)
+r_1(X) :- +v(X), ¬r_1(X), ¬r_2(X)
```
つまり，$ΔS := putdelta(S, V)$ ではなく “$ΔS := putdelta(S, ΔV)$” という具合の定式化になる？
## DatalogプログラムとSQLクエリの対応
資料によると，以下のようなviewの定義を，
```
R(p, X) <- P_1(Y_1), …, P_n(Y_n), Cond_1, …, Cond_o, ¬N_1(Z_1), …, ¬N_m(Z_m)
```
変換した結果が以下のSQL文らしい：
```
CREATE VIEW R AS
SELECT p, x_1, …, x_x FROM (
SELECT p, x^1, …, x^j FROM P_1, …, P_n
WHERE ∀i∀j ∈ {1, …, n}. (i < j ⇒ ∀y ∈ FV(Y_i) ∩ FV(Y_j). P_i.y = P_j.y) ∧ Cond_1 ∧ … ∧ Cond_o
∧ (NOT EXISTS (SELECT * FROM N_1 WHERE N_1.z^1 = P_1.y^1 ∧ … ∧ N_1.z^k = P_j.y^l))
∧ …
∧ (NOT EXISTS (SELECT * FROM N_m WHERE …))
) UNION (…)
```
どうやらpositiveな原子式は2個ずつで等式制約にするらしい？
添えられている例も見てみる：
```
+eed(E, D) :- ed(E, D), D = 'A', ¬eed(E, D).
-eed(E, D) :- ed(V1, D), eed(E, D), E = 'Joe', D = 'A', ¬eed(V1, D).
+ed(E, D) :- ed(V1, D), E = 'Joe', D = 'A', ¬ed(E, D), ¬eed(V1, D).
```
`eed` がviewで `ed` がsource databaseっぽい？
- 1行目： 「部署が `A` の社員情報が `ed` にあって `eed` にない場合は `eed` に追加」
- 2行目： 「或る `V1` に対して `(V1, 'A')` が `ed` にあるが `eed` に含まれていない場合，`('Joe', 'A')` が `eed` にあるなら `eed` から消す」
- 3行目： 「或る `V1` に対して `(V1, 'A')` が `ed` にあるが `eed` に含まれていない場合，`('Joe', 'A')` が `ed` にないなら `ed` に追加」
上2行はview `eed` の定義のようなもので，3行目はviewの更新に基づくsource databaseの更新の定義．しかし，変換後のSQLから見るに本来以下のようなものではないか？
```
+eed(E, D) :- ed(E, D), D = 'A', E != 'Joe', ¬eed(E, D).
-eed(E, D) :- ed(V1, D), eed(E, D), E = 'Joe', D = 'A', V1 != 'Joe', ¬eed(V1, D).
+ed(E, D) :- ed(V1, D), E = 'Joe', D = 'A', V1 != 'Joe', ¬ed(E, D), ¬eed(V1, D).
```
要するに
- 「`('Joe', 'A')` を除く，部署が `A` の社員情報が `ed` にあって `eed` にない場合，それを `eed` に追加」
- 「`'Joe'` 以外の或る `V1` に対して `(V1, 'A')` が `ed` にあるが `eed` に含まれていない場合，`('Joe', 'A')` が `eed` にあるなら `eed` から消す」．
- …
```sql
CREATE TEMPORARY TABLE p_eed AS
SELECT emp_name, dept_name FROM ed WHERE
// positive部分はSELECTのみ．positiveな原子式が1つしかないため
// Cond部分：
dept_name = 'A' AND emp_name != 'Joe'
// negative部分：
AND NOT EXISTS (SELECT * FROM eed WHERE ed.emp_name = eed.emp_name AND ed.dept_name = eed.dept_name);
```
2行目に基づいて eed から消すものを列挙するクエリ：
```sql
CREATE TEMPORARY TABLE m_eed AS
SELECT ed.emp_name, ed.dept_name FROM ed, eed WHERE
// positive部分（ed(V1, D) と eed(E, D) に関して．dept_name = D ∈ {V1, D} ∩ {E, D}）：
ed.dept_name = eed.dept_name
// Cond部分：
AND eed.emp_name = 'Joe' AND ed.dept_name = 'A' AND ed.emp_name != 'Joe'
// negative部分（¬eed(V1, D) に基づく）：
AND NOT EXISTS (SELECT * FROM eed WHERE eed.emp_name = ed.emp_name AND eed.dept_name = ed.dept_name);
```
`ed(V1, D)` から `V1` が `ed.emp_name` に，`D` が `ed.dept_name` に相当することになる？ しかしだとすると2行目のSELECT文は `SELECT eed.emp_name, …` にならないとおかしい．誤植？ 修正した上で `AS` でタプルに別名をつけると以下のようになる：
```sql
CREATE TEMPORARY TABLE m_eed AS
SELECT /* E := */ y.emp_name, /* D := */ x.dept_name FROM ed AS x, eed AS y WHERE
// positive部分（ed(V1, D) と eed(E, D) に関して．dept_name = D ∈ {V1, D} ∩ {E, D}）：
x.dept_name = y.dept_name
// Cond部分：
AND y.emp_name = 'Joe' /* E = 'Joe' */
AND x.dept_name = 'A' /* D = 'A' */
AND x.emp_name != 'Joe' /* V1 != 'Joe' */
// negative部分（¬eed(V1, D) に基づく）：
AND NOT EXISTS (SELECT * FROM eed AS z WHERE z.emp_name = x.emp_name AND z.dept_name = x.dept_name);
```
なるほど，だいたいわかった．一応3行目に対応するSQL文も見ておく：
```sql
CREATE TEMPORARY TABLE p_ed AS
SELECT /* E := */ text 'Joe' AS emp_name, /* D := */ ed1.dept_name FROM ed AS ed1 WHERE
// positive部分はSELECTのみ．positiveな原子式が1つしかないため
// Cond部分（E = 'Joe' は SELECT に組み込まれているらしい）：
ed1.dept_name = 'A' /* D = 'A' */
AND ed1.emp_name != 'Joe' /* V1 != 'Joe' */
// negative部分：
AND NOT EXISTS (SELECT * FROM ed AS ed2 WHERE ed2.emp_name = 'Joe' AND ed2.dept_name = ed1.dept_name)
AND NOT EXISTS (SELECT * FROM eed WHERE eed.emp_name = ed1.emp_name AND eed.dept_name = ed1.dept_name)
```
`E` が定数展開されている具合らしい．大体わかった．
## 完全に理解した
ruleからSQL文への変換アルゴリズムを，以下の例を使って説明する：
```
+ed(E, D) :- ed(V1, D), E = 'Joe', D = 'A', V1 != 'Joe', ¬ed(E, D), ¬eed(V1, D).
```
1. まずrule headを見て，最終的に必要な変数とそれに対応するカラム名の組 $(X_1, l_1), …, (X_n, l_n)$ を知る．
- 上記の例なら，`+ed(E, D)` がrule headなので `E` と `D` が最終的に必要な変数で，カラム名は省略しているが `emp_name` と `dept_name`．
2. rule bodyのpositiveな命題それぞれにフレッシュなインスタンス名を割り振る．
- 上記の例なら，`ed(V1, D)` が唯一のpositiveな命題で，これに対応するインスタンスに `ed1` という名前を割り当てる．
3. rule bodyのpositiveな命題の列とconditionの列を走査し，各変数にテーブルとカラム名（または定数）を紐づける．この紐づけを $f$ とおく．
- 上記の例なら，まず `V1` が `ed1.emp_name` であると紐づけられ，続いて `D` が `ed1.dept_name` であると紐づけられる．そして `E` はpositiveな命題に出現せずconditionから `'Joe'` という定数に紐づくとわかる．
- このとき，変数ごとに一般には複数のテーブルのカラムに対応することがあるが，そのうちの1つを使えばよく，残りは等式制約 $E_1, \ldots, E_m$ になる．
4. 1の変数 $X_1$, …, $X_n$ と3で生成した紐づけ $f$ を用いて $\text{SELECT}\ f(X_1)\ \text{AS}\ l_1, \ldots, f(X_n)\ \text{AS}\ l_n$ をSELECT句とする．
- 上記の例なら，`SELECT text 'Joe' AS emp_name, ed1.dept_name AS dept_name`．
5. 4でできたSELECT句に出現するインスタンスを集めてFROM句とする．「テーブル名 AS インスタンス名」の列挙．
- 上記の例なら，`ed1` のみがSELECT句に出現するので `FROM ed AS ed1`．
6. 3でできた等式制約の列 $E_1, \ldots, E_m$ と，もともとのconditionの列 $C_1, \ldots, C_k$ から3で使われた等式を除去した列と，各negativeな命題に対応する制約の列を並べてWHERE句とする．
- negativeな命題 $¬r(l^{\prime}_1 = X^{\prime}_1, \ldots, l^{\prime}_a = X^{\prime}_a)$ の変換は簡単で，単に $\text{NOT EXISTS}\ (\text{SELECT}\ \ast\ \text{FROM}\ r\ \text{AS}\ I\ \text{WHERE}\ I.l^{\prime}_1 = f(X^{\prime}_1)\ \text{AND}\ \cdots\ \text{AND}\ I.l^{\prime}_a = f(X^{\prime}_a))$ とすればよい．
- 上記の例なら，まず等式制約は空列．conditionの列のうち `E = 'Joe'` は既に3で使用したので，これ以外の `D = 'A'` と `V1 != 'Joe'` がWHERE句に残る．negativeな命題はそれぞれ `NOT EXISTS (SELECT * FROM ed AS ed2 WHERE ed2.emp_name = 'Joe' AND ed2.dept_name = ed1.dept_name)` と `NOT EXISTS (SELECT * FROM eed WHERE eed.emp_name = ed1.emp_name AND eed.dept_name = ed1.dept_name)`．
## 既存のBIRDSの実装のどこをいじるべきか
基本的には `Ast2sql` に生やすとよさそう．`Expr` には以下のような型が定義されている：
```ocaml
type rule = rterm * term list
```
rule を表す型．rule headが1要素目，rule bodyが2要素目：
```ocaml
type rterm =
| Pred of string * var list (* r(X_1, …, X_n) 相当 *)
| Deltainsert of string * var list (* +r(X_1, …, X_n) 相当 *)
| Deltadelete of string * var list (* -r(X_1, …, X_n) 相当 *)
```
atomic formulaを表す型．
```ocaml
type var =
| NamedVar of string
| NumberedVar of int (* よくわからない．構文解析で得られるものではないらしい *)
| ConstVar of const (* 定数 *)
| AnonVar (* 無名変数 *)
| AggVar of string * string (* aggregationの適用．sum や avg など *)
```
`var` という型名だが，正確にはatomic formulaの実引数を表す型．`NamedVar` と `ConstVar` が基本．`AnonVar` は無名変数らしいが，フレッシュに生成して `NamedVar` に合流してよさそうではある．`NumberedVar` はよくわからないが，元のコメントによると構文解析で得られるものではないらしく，内部表現用らしい？ どうやら構文解析の結果と内部表現とを分けて扱っていないのかも．`AggVar` は今回は関係なさそう．
```ocaml
type term =
| Rel of rterm (* positiveな命題 *)
| Not of rterm (* negativeな命題 *)
| Equat of eterm (* 比較式 *)
| Noneq of eterm (* 比較式の否定？ おそらく単に構文的に NOT がついたもの *)
```
rule bodyの各要素の形式．positiveな命題，negativeな命題，conditionの3つがある（後ろ2つは構文的な違いだけで，conditionとして共通化してよいはず）．
```ocaml
type eterm =
| Equation of string * vterm * vterm (* string is one of '=', '<>', '<', '>', '<=', '>=' *)
```
比較式（`Equation` といっているが不等式も含む）．
```ocaml
type vterm =
| Const of const
| Var of var
| BinaryOp of string * vterm * vterm (* string is one of '+', '-', '*', '/', '^' *)
| UnaryOp of string * vterm (* string is one of '-' *)
```
比較式中で使われる，値の式．`Var (ConstVar _)` と `Const _` はダブってる気がする．
Sign in with Wallet
Connect another wallet