エルブラン・セマンティクス(Herbrand Semantics)理解メモ

はじめに

データベースのトランザクション（特にスケジュール）の理論を勉強しようとすると、エルブラン・セマンティクス(Herbrand Semantics)の理解が必要となります。

Herbrand Semantics の解説は以下の本・章にあります。

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems)

該当章：3.5 Herbrand Semantics of Schedules

ですが、本が英語であることに加え、読み解くには数学の知識も必要となります。そこで、周辺知識を含めて理解していく過程をエントリにまとめることにしました。

解説

ここではトランザクションが失敗（ロールバック）することを考えません。

次のようなスケジュールsを仮定します。

1. a step r_i(x) ∈ s of a transaction t_i ∈ trans(s) reads the value written by the last w_j(x) ∈ s, j ≠ i, that occurs before r_i(x);
2. a step w_i(x) ∈ s writes a new value that potentially depends on the values of all data items that t_i has read from the database or from other transactions in active(s) ∪ commits(s) prior to w_i(x).

ここでは以下のことを仮定しています。

1. r_i(x)は最後にwriteされた値xをreadする。
2. w_i(x)はそのトランザクションt_iがw_i(x)の前にreadした全ての値に依存している。

DEFINITION 3.3 Herbrand Semantics of Steps

Let s be a schedule. The Herbrand semantics H_s of steps r_i(x), w_i(x) ∈ op(s) is recursively defined as follows:

1. H_s(r_i(x)) := H_s(w_j(x)), where w_j(x), j ≠ i, is the last write operation on x in s before r_i(x).
2. H_s(w_i(x)) := f_ix(H_s(r_i(y₁)),...,H_s(r_i(y_m))), where the r_i(y_j), 1 ≤ j ≤ m, represent all read operations of t_i that occur in s before w_i(x), and where f_ix is an uninterpreted m-ary function symbol.

H_s は Herbrand semantics のことです。

1. H_s(r_i(x)) := H_s(w_j(x))

H_s(r_i(x)) を H_s(w_j(x))と定義するということです。
参考：数学記号の表 - Wikipedia
r_i(x) は w_j(x) に等しい、つまり最後にwriteした値をreadする、ということです。

2. H_s(w_i(x)) := f_ix(H_s(r_i(y₁)),...,H_s(r_i(y_m)))

"m-ary function"とは「m項関数」と呼ばれ、m個の引数をもつ関数のことです。

関数f_ixの"i"はトランザクションT_iのこと、"x"は値xのことです。
関数f_ixの引数はトランザクションT_iでw_i(x)以前の全てのread操作のH_sです。

ここでのポイントは read/write が m-ary function に変換可能ということにあります。

例えば、次のスケジュールを考えます。
s = r₁(x)r₂(y)w₂(x)w₁(y)c₂c₁

値x, yには初期値があるはずです。これをトランザクションt₀が書き込んだものと仮定すれば、次のスケジュールになります。
s = w₀(x)w₀(y)c₀r₁(x)r₂(y)w₂(x)w₁(y)c₂c₁

これを踏まえて以下の展開を行います。

s = w₀(x)w₀(y)c₀r₁(x)r₂(y)w₂(x)w₁(y)c₂c₁

is as follows, where f_0x() and f_0y() are 0-ary functions (constants):

H_s(w₀(x)) = f_0x()
H_s(w₀(y)) = f_0y()
H_s(r₁(x)) = H_s(w₀(x)) = f_0x()
H_s(r₂(y)) = H_s(w₀(y)) = f_0y()
H_s(w₂(x)) = f_2x(H_s(r₂(y)) = f_2x(f_0y())
H_s(w₁(y)) = f_1y(H_s(r₁(x)) = f_1y(f_0x())

Herbrand semantics H_s を展開していくと、どのread/writeもf_0x()/f_0y()を含む関数の式に変換されます。つまり、read/writeを初期状態と関数の式で表現できたということであり、異なるスケジュールのトランザクションの各ステップ(read/write)が同じ結果となるかを数式で比較可能となります。Herbrand semantics で表現することの価値はここにあります。

具体例については以下の記事を参照ください。
Serializablitiyとは？ １. Final State Serializabilityについて - Qiita
Serializablitiyとは？ 2. View Serializabilityについて - Qiita
Herbrand Semantics の式の表現は異なりますが、実現していることは同じです。

DEFINITION 3.4 Herbrand Universe

Let D = {x, y, z,...} be a (finite) set of data items (representing the data of the underlying data server(s)). For a transaction t, let op(t) denote the set of all steps of t. The Herbrand universe HU for transactions t_i, i > 0, is the smallest set of symbols satisfying the following conditions:

1. f_0x() ∈ HU for each x ∈ D, where f_0x is a 0-ary function symbol (i.e., a constant);
2. if w_i(x) ∈ op(t_i), |{r_i(y) | (∃y ∈ D) r_i(y) <_ti w_i(x)}| = m, and if v₁,..., v_m ∈ HU, then f_ix(v₁,...,v_m) ∈ HU, where f_ix is an m-ary function symbol.

"{r_i(y) | (∃y ∈ D) r_i(y) <_ti w_i(x)}"は集合の内包的記法です。
{ (代表元) | (代表元の満たすべき条件)} です。例えば {x | x ∈ S, P(x)} は S の元のうち、命題 P(x) が真であるものすべてを集めた集合を意味しています。
参考：数学記号の表 - Wikipedia

また、集合Aの要素数は|A|で表現されます。例えば、A={1,2,3,4}, |A|=4です。
参考：集合の要素数

つまり、"|{r_i(y) | (∃y ∈ D) r_i(y) <_ti w_i(x)}| = m"とはT_iがw_i(x)の前にreadした回数をmとする、ということです。

これを踏まえて DEFINITION 3.4 をまとめると、

1. f_0xは0項関数で定数だ。
2. f_ixはm項関数（m個の引数を持つ）で、mはT_iがw_i(x)の前にreadした回数に等しい。

となります。

2.でf_ixとw_i(x)の関係がピンとこない場合は DEFINITION 3.3を再確認してください。下記の式で w_i(x)の Herbrand Semantics は f_ixの関数で表現されることが示されています。
H_s(w_i(x)) := f_ix(H_s(r_i(y₁)),...,H_s(r_i(y_m)))

DEFINITION 3.5 Schedule Semantics

The semantics of a schedule s is the mapping

H[s] : D → HU

defined by

H[s](x) := H_s(w_i(x))

where w_i(x) is the last operation from s writing x, for each x ∈ D.

"H[s] : D → HU"とは写像の表記です。

写像とは"f : A → B"の形で表現され、Aの要素が決まるとBの要素が決まる対応関係です。
"f(A) = B"のように、fはAを引数にとってBとなる、と考えるとわかりやすいかもしれません。
参考：写像とは

つまり、"H[s](x) := H_s(w_i(x))"は "H[s](x)" がスケジュールsの値xの最終的な状態（最後のwrite操作）を Herbrand Semantics で表現する、ということを表しています。

s = w₀(x)w₀(y)c₀r₁(x)r₂(y)w₂(x)w₁(y)c₂c₁

H[s](x) = H_s(w₂(x)) = f_2x(f_0y())
H[s](y) = H_s(w₁(y)) = f_1y(f_0x())
※引用に際して一部省略

この例でスケジュールsの値xに対する最後のwrite操作はw₂(x)、値yに対する最後のwrite操作はw₁(y)であり、H[s](x), H[s](y) は これらのwrite操作を Herbrand Semantics で表現するということです。