英語の技術書の解説みたいなのをブログに書くときに、書中にちゃんと書いてありますよ~これが証拠ですよ〜という風な感じで、どかっと英文を乗せることがある。例えば以下の記事。

分かりやすさのために載せているのではなく、証拠として載せてるものが本文中にいきなり引用スタイルでどかっと出てきて、文章のリズムみたいなのが悪くなって分かりやすさを下げているように思える。

改善

改善のための工夫として、"証拠"として載せている文章は引用スタイルをやめて全て脚注にまとめてみた。分かりやすさのために載せているものはそのままにした。これで、文章を変に重くしている英語の文章が減って読みやすくなっているように思える。

総評
- 脚注には本中に対応するページ数が欲しい
- はてなの記法((脚注文章))だと脚注の文章には丸括弧を含めることができない
- 丸括弧を使いたいなら脚注はmarkdown方式[^1]で書く必要がある
- 英語の引用が減ったため、パワー不足を感じる。
  - もう少し日本語だけでわかるような説明にするべき。
以下見やすさのテストスタート

herbrand semanticsのメモです。主にFSRを理解するための準備です。このエントリはpapa本の5~9ページのまとめです。

transactionとreadとwrite
interpretation
同じentityへの各database stepは1回まで
Interpretationとshcedule
まとめ

データベースの世界にはherbrand semanticsというConflictやSerializabilityを考える時に使う便利な道具があります。いつからherbrand semanticsと呼ばれるようになったのかはわかりませんが、Christos Papadimitrioupapa:Theory of Database Concurrency Control(通称papa本)ではinterpretationという名前で扱われています。近年ではトランザクションの教科書にもherbrand semanticsと書かれていることもありますので、本エントリではpapa本からの引用以外はこちらの名前を使います。

weikum本寄りの解説はぱとさんがあげているので、今回はpapa本寄りのメモを書きたいと思います。

taityo-diary.hatenablog.jp

Theory of Database Concurrency Control

作者: Christos Papadimitriou
出版社/メーカー: Computer Science Pr
発売日: 1986/07/01
メディア: ハードカバー
この商品を含むブログを見る

transactionとreadとwrite

まずはトランザクションの定義から。トランザクションは任意のentityに対するreadとwriteの有限集合。　*1

read:対象entityの現在の値をプログラム中の変数へ割当てることを意味する。*2
write:対象entityに対するプログラムで計算した値の割り当てを意味する。*3

なおこのwriteで書く値の計算はwrite step以前のすべてのreadを引数にとる関数fとして定義することができる。この関数の厳密な定義がherbrand semanticsになる。

interpretation

条件分岐や繰り返しなどの制御構文を含むアプリ(プログラム)から発行されたdatabaseに対するread/writeのdatabase stepの意味をdatabase側から解釈する。プログラムが発行したdatabase stepのまとまりはtransactionになる。transactionは制御構文を持たないので、アプリとは別の解釈が必要となる。*4

トランザクションの実行はある状態からある状態への写像と解釈する。*5

$f_a: \prod_{x \in B(a)} D_x \to D_{ENTITY(a)}$

writeのオペレーションはそれまでに読んだ値のドメインの直積からwrite対象のentityのドメインへの写像になる。
B(a)はa以前に読んだ全てのentityの集合。

$B(a_j) = {x \in E : {\bf For \, some }\, i \le j \, ACTION(a_i) = {\bf R \, and \, }ENTITY(a_i) = x}$

具体例として1トランザクション前提(1並列)で以下の送金プログラムで説明されている。

program transfer(amt:integer);
    entities x,y: integer;
    variables temp1,temp2:integer;
    begin
    temp1 := x;
    if temp1 ≧ amt then
        begin
        x := tmp1 -amt; 
        temp2 := y;
        y := temp2 + amt
        end
    end.

ローカル変数へのentity代入をread,entityへの値の書き込みをwriteのデータベースステップと考えると上記のプログラムは以下のschedule(Action)を作る。

A = R(x)W(x)R(y)W(y)

この時、各database stepのherbrand semanticsは以下のようになる。

t1:=x
x:=f2(t1)
t3:=y
y:=f4(t1,t3)

f4の関数の内容はf4(t1,t3)=t3+50で、t1は一切使わないが、このt1はherbrand semanticsでは必要とする。どのパラメータが実際に使われているかという情報はアプリ(DBMSを読み書きするプログラム)の完全な情報がないと分からない。そしてconncurency controlを考える時にアプリのコード全体が把握できるケースは極めて稀*6であるため、writeの前に発行されたreadは全てwriteを表す関数の引数として扱う。*7

同じentityへの各database stepは1回まで

オペレーションごとにherbrand semanticsを考えることができそうだが、correctなスケジュールなら1つのentityへの複数回のread,writeは冗長なので、herbrand semanticsを考えるときは同じトランザクション内では

read/writeは1つのentityに対して1回まで
writeしたentityの値をreadしない

という前提を置く*8 *9 *10

後述しますが、本来ならあるトランザクションの何番目のステップのfというような表記になるところを上記の前提を置くことで、あるトランザクションのあるentityに対する操作(f)、またはあるトランザクションの何番目の操作(f)というシンタックスで表現できる。ちなみに、weikum本では前者のシンタックスを採用し、papa本では後者を採用している。*11

Hs(wi(x)) := fix(Hs(ri(y1)),...,Hs(ri(ym))), where the ri(yj), 1 ≤ j ≤ m, represent all read operations of ti that occur in s before wi(x)

weikum本より引用。 $f_{ix}$ のiをトランザクションの添え字、xをentityとするシンタックスにしている

Interpretationとshcedule

トランザクション1つにつき一つのinterpretationがある。
sheduleは1個以上のトランザクションの集合だから、shedule sのIntrepretationはsに含まれる全てのtransactionの集合になる。*12

scheduleにinterpretationを適応すると、schedule中の任意のdatabase stepを $a_s(I,X)$ で表現することができる。*13

また、スケジュールの実行結果、つまり最終状態をs(I,X)という特別なシンタックスで表現する*14

まとめ

各entityがとりうる値(domain)の集合をDとしている
writeの関数fのすべての集合をFとしている。
上記二つのペアをinterpretation(herbrand semantics)としている。
- interpretationと初期値Xを使うことでtransaction中の任意のstepを関数で表現できる

*1:Difinition 1.1 A transaction A is a finite sequence fo steps A = a_1,a_2...a_n. The steps are assumed to be distinct symbols, and two differencttransactions cannot have steps in common. With each step a_j of A we associate an action ACTION(a_j) ∈ {W,R}, and an entity ENTITY(a_j) ∈ E.

*2:If some step a_j reads entity x. This means that a particular program variable t_j in the underlying program is assigned the current value of x in the database: t_j := x.

*3:If ACTION(a_j) = W and ENTITY(a_j) = x , then the step write x. By this we mean that x is assigned a value computed by the program, which is potentially a function of all previously read(by the same program) values of entities: x := fj(t_i1,ti_2,...t_ik),where the ip's are all indices smaller than j for which ACTION(a_ip) = R

*4:A transaction, as defined above, is a purely syntactic object, subject to different interpretations. Intuitively, specifying an interpretation of a transaction means fixing a particular application program from which the transaction has originated, disregarding of course any control structure the program may have.

*5:An interpretation of A(注:このAは任意のtransactionを指している) is a pair I = (D,F), where D = {D_x,D_y,...} is a set of domains, onefor each entity in E; each domain is a set of values for the corresponding entity. F = {f_a:a is a step of A and Action(a)=W} is a set of functions, one for each write step of A. For each such step a, f_a is a mapping

*6:ストアドは例外

*7:Situations such as this of Example 1.2, in which we have complete information about the program and the value of their parameters, are rare in concurrency control

*8:It is quite natural-and, it turns out, simplifying-to make the following assumptions about the structure of the transactions.

*9:a:In a transaction an entity is read at most once, and is written at most once.

*10:b:In a transaction, no entity is read after it is written.

*11:上記のプログラムのread/writeへのherbrand semanticsの適当を見ると、最初のwriteは2回目のオペレーションなのでf2となっている

*12:If s is a schedule involving the transactions A_1,...,A_k, then an interpretation I of s is a k-tuple of interpretations I_j = (D,F_j), all with the same choice D of domains for the entities.

*13:Suppose that s is a schedule, I an interpretation, and X an initial state, that is a value for each entity. We say that every database step a of s computes a value a_s(I,X).

*14:The final state resulting from the execution of s, denoted s I,X