タプル関係計算

計算体系は関係データベースのクエリ言語であるため、まず関係データベースを定義する必要があります。関係の基本的な構成要素はドメイン（データ型と多少似ていますが、同一ではありません）です。タプルは、ドメインと値の順序付きペアである属性の有限シーケンスです。リレーションは、（互換性のある）タプルの集合です。これらの関係概念は数学的に定義されていますが、これらの定義は従来のデータベース概念に大まかに対応しています。テーブルは、リレーションの視覚的な表現として受け入れられています。タプルは、行の概念に似ています。

まず、列名の集合Cが存在すると仮定します。その例としては、「name」、「author」、「address」などがあります。ヘッダーはCの有限部分集合として定義します。リレーショナルデータベーススキーマは、タプルS = ( D、R、h )として定義されます。ここで、 Dは原子値のドメイン (ドメインと原子値の概念の詳細については、リレーショナルモデルを参照)、Rは関係名の有限集合、

h  : R → 2 ^C

Rの各リレーション名にヘッダーを関連付ける関数。（これは、ドメインが複数あり、ヘッダーが単なる列名のセットではなく、これらの列名をドメインにマッピングする完全なリレーション モデルからの簡略化であることに注意してください。）ドメインDが与えられた場合、 D上のタプルを、いくつかの列名をDの原子値にマッピングする部分関数として定義します。例としては、（name : "Harry", age : 25）などがあります。  

t  : C ⇸ D

D上のすべてのタプルの集合はT _Dと表記されます。タプルtが定義されているCの部分集合はtのドメインと呼ばれ(スキーマのドメインと混同しないように注意)、dom ( t ) と表記されます。

最後に、スキーマS = ( D , R , h ) が与えられた場合のリレーショナルデータベースを関数として定義します。

db  : R → 2 ^{T _D}

これは、 R内の関係名をT _Dの有限部分集合にマッピングし、 R内のすべての関係名rとdb ( r )内のタプルtに対して、以下が成り立つ。

dom ( t ) = h ( r )。

後者の要件は、リレーション内のすべてのタプルが同じ列名、つまりスキーマで定義されている列名を持つべきである、ということを単純に述べている。

式の構築にあたっては、タプル変数の無限集合Vを仮定します。式は、データベーススキーマS = ( D , R , h ) と、型割り当て時に呼び出される部分関数 型V ⇸ 2 ^C が与えられたときに定義され、この関数はいくつかのタプル変数にヘッダーを割り当てます。次に、原子式の集合A [ S , type ] を次の規則で定義します。

1. vとwがVに属し、a が型( v )に属し、 b が型( w )に属する場合、式v . a = w . bはA [ S , type ]に属します。
2. v がVに属し、a が型( v )に属し、 kがDの値を表す場合、式v . a = kはA [ S , type ]に属し、
3. v がVに属し、r がRに属し、型( v ) = h ( r ) であるならば、式r ( v ) はA [ S , type ] に属します。

原子の例としては、以下のようなものがあります。

• ( t.age = s.age ) — tにはage属性があり、sにはage属性があり、その値は同じである。
• ( t .name = "Codd") — タプルtには name 属性があり、その値は "Codd" です
• Book( t ) — タプルtは関係Bookに存在します。

このようなアトムの形式意味論は、 S上のデータベースdbと、タプル変数をSのドメイン上のタプルにマッピングするタプル変数バインディングval : V → T _Dが与えられたときに定義されます。 

1. v . a = w . b は、 val ( v )( a ) = val ( w )( b ) の場合に限り真となります。
2. v . a = k は、 val ( v )( a ) = k の場合に限り真となる。
3. r ( v )は、 val ( v )がdb ( r )に含まれる場合に限り真である。

原子は、一階述語論理で通常行われるように、論理演算子 ∧ (かつ)、∨ (または)、¬ (否定) を用いて式に組み合わせることができ、存在量化子 (∃) と全称量化子 (∀) を用いて変数を束縛することができます。式の集合F [ S , type ] を、以下の規則に従って帰納的に定義します。

1. A [ S、タイプ]のすべての原子はF [ S、タイプ]にも含まれています
2. F ₁とF _2がF [ S , type ]に含まれる場合、式 F ₁ ∧ F _2もF [ S , type ] に含まれる。
3. F ₁とF _2がF [ S , type ]に含まれる場合、式 F ₁ ∨ F _2もF [ S , type ] に含まれる。
4. FがF [ S、タイプ]に含まれる場合、式 ⁠${\displaystyle \neg F}$⁠はF [ S、タイプ] にも含まれています
5. v がVに含まれ、H がヘッダー、FがFに含まれる式である場合[ S、タイプ_{[ v → H ]} ] 式⁠${\displaystyle \exists v:H(f)}$⁠はF [ S、 type ]にも含まれており、ここでtype _{[ v → H ]は、} vをHにマッピングすることを除いてtypeと等しい関数を表します。
6. v がVに含まれ、H がヘッダー、FがFに含まれる式である場合[ S、タイプ_{[ v → H ]} ] 式⁠${\displaystyle \forall v:H(f)}$⁠はF [ S、タイプ]にも含まれています

数式の例：

• t.name = "CJ Date" ∨ t.name = "H. Darwen"
• 書籍( t ) ∨ 雑誌( t )
• ${\displaystyle \forall t:\{{\text{著者、タイトル、主題}}\}(\neg ({\text{Book}}(t)\wedge t{\text{.author}}=}$「CJ日付」${\displaystyle \wedge \ \neg (t{\text{.subject}}=}$「関係モデル」${\displaystyle )))}$

最後の式は、CJ Dateが執筆したすべての書籍の主題が関係モデルであることを示しています。通常どおり、式の意味に曖昧さが生じない場合は括弧を省略します。

量化子はスキーマ内のドメイン上のすべてのタプルの全体にわたって量化すると仮定します。これにより、S上のデータベースdbとタプル変数バインディングval : V → T _D :が与えられた場合の式に対する次の形式意味論が得られます。 

1. F ₁ ∧ F _2は、 F _{1が真であり、かつ}F ₂が 真である 場合に限り 真である。
2. F ₁ ∨ F _2は、 F ₁が真であるか 、 F ₂ が真であるか、または両方が真である 場合に限り
3. ⁠${\displaystyle \neg f}$⁠ は、F が真でない 場合に限り真である
4. ⁠${\displaystyle \exists v:H(f)}$は、 D上の タプルtが存在してdom ( t ) = Hであり、かつ式 Fがval _{[ v → t ]} に対して真で、
5. ⁠${\displaystyle \forall v:H(f)}$⁠ は、 dom ( t ) = HとなるD上のすべてのタプルtに対して、 val _{[ v → t ]}に対して式 F が真である場合に限り真である。

最後に、スキーマS = ( D , R , h ) が与えられた場合のクエリ式がどのようなものになるかを定義します。

{ v  : H | f ( v ) }

ここで、vはタプル変数、Hはヘッダー、f ( v ) はF [ S , type ]の式であり、 type = { ( v , H ) } で、vは唯一の自由変数です。S上の特定のデータベースdbに対するこのようなクエリの結果は、 dbに対してf が真であり、val = { ( v , t ) }であるような、dom ( t ) = HであるD上のすべてのタプルtの集合です。

クエリ式の例は次のとおりです。

量指定子のセマンティクスは、スキーマ内のドメイン上のすべてのタプルに対して量指定を行うため、別のスキーマを想定した場合、クエリが特定のデータベースに対して異なる結果を返す可能性があります。たとえば、ドメインがD 1 = { 1 }、D 2 = { 1, 2 _}、リレーション名_がR = { r 1 } 、ヘッダーがh = { ( r 1 , { a }) } である 2 つのスキーマ S 1 = ( D 1 , R , h ) と S 2 = ( _D 2 , R _{, h} )を_考えてみましょう。どちらの_スキーマにも共通のインスタンス_があります。

db = { ( r ₁ , { ( a , 1) } ) }

次のクエリ式を考慮すると

{ t  : {a} | t .a = t .a }

この場合、データベースに対する結果は、 S _{1 の}下では { (a  : 1) }またはS ₂の下では { (a : 1), (a : 2) } のいずれかになります。ドメインを無限集合とすると、クエリの結果も無限になることは明らかです。これらの問題を解決するために、ドメインに依存しないクエリ、つまり、データベースのすべてのスキーマの下で同じ結果を返すクエリにのみ注目します。  

これらのクエリの興味深い特性は、タプル変数がデータベースのいわゆるアクティブドメイン（データベース内またはクエリ式内の少なくとも1つのタプルに出現するドメインのサブセット）上のタプルを対象とすると仮定した場合、クエリ式の意味論は変化しないという点です。実際、タプル計算の多くの定義では、このようにして量化子の意味論が定義されており、これによりすべてのクエリは定義上ドメインに依存しないものとなります。

クエリ式がドメインに依存しないクエリのみを表現するように制限するために、通常は安全なクエリの構文概念が導入されます。クエリ式が安全かどうかを判断するために、クエリから 2 種類の情報を導き出します。1 つ目は、変数と列のペアt . aがリレーションの列または定数に束縛されているかどうか、2 つ目は、2 つの変数と列のペアが直接的または間接的に等しくなっているかどうか ( t . v == s . wと表記) です。

有界性を導出するために、以下の推論規則を導入する。

1. v.a = w.bでは変数列のペアが束縛されていません。
2. v . a = k では、変数列ペアv . aは束縛されます。
3. r ( v )では、すべてのペアv . a は型( v )のaに束縛されます。
4. f ₁ ∧ f ₂では、f ₁またはf ₂のいずれかで束縛されているすべてのペアが束縛されている。
5. f ₁ ∨ f ₂では、f ₁とf ₂の両方で束縛されているすべてのペアが束縛されている。
6. で⁠${\displaystyle \neg f}$ペアはバインドされていません。
7. で⁠${\displaystyle \exists v:H(f)}$ペアw . a は、 fで束縛され、 w ≠ vである場合に束縛される。
8. で⁠${\displaystyle \forall v:H(f)}$ペアw . a は、 fで束縛され、 w ≠ vである場合に束縛されます。

等価性を導出するために、以下の推論規則を導入します（通常の同値関係の推論規則である反射律、対称律、推移律に加えて）。

1. v . a = w . bでは、 v . aはw . bと等しいことが成り立ちます。
2. v . a = kではペアは等しくありません。
3. r ( v )ではペアは等しくありません。
4. f ₁ ∧ f ₂において、 v . aがw . bと等しいのは、 f ₁またはf ₂のいずれかで成り立つ場合である。
5. f ₁ ∨ f ₂において、v . aがw . bと等しいのは、 f ₁とf ₂の両方で成り立つ場合である。
6. で⁠${\displaystyle \neg f}$ペアは等しくありません。
7. で⁠${\displaystyle \exists v:H(f)}$fにおいてw ≠ vかつx ≠ vが成り立つ場合、w . aはx . bと等しいとみなされ、
8. で⁠${\displaystyle \forall v:H(f)}$⁠ fにおいてw ≠ vかつx ≠ vの場合、 w . aはx . bと等しいとみなされます。

クエリ式は次のように定義されます。${\displaystyle \{v:H\mid f(v)\}}$⁠は安全です

• Hのすべての列名aに対して、 v . aはfの束縛ペアと等しいことが導き出されます。
• fのすべての部分式に対して、${\displaystyle \forall w:G(g)}$⁠ Gのすべての列名aに対して、 w . aはgの束縛ペアと等しいが導き出され、
• fのすべての部分式に対して、${\displaystyle \exists w:G(g)}$⁠ Gのすべての列名aに対して、 w . aはgの束縛ペアと等しいが導き出せる。

安全なクエリ式への制限は表現力を制限するものではありません。なぜなら、表現可能なすべてのドメイン非依存クエリは、安全なクエリ式によっても表現できるからです。これは、スキーマS = ( D , R , h )、クエリ式内の定数の集合K 、タプル変数v、およびヘッダーHに対して、値がアクティブドメインにあることを示す、 H内のaを含むすべてのペアv . aの安全な式を構築できることを示すことで証明できます。たとえば、K ={1,2}、R ={"r"}、h = { ("r", {"a, "b"}) } と仮定すると、 v .bに対応する安全な式は次のようになります。

${\displaystyle v{\text{.b}}=1\vee v{\text{.b}}=2\vee \exists w(r(w)\wedge (v{\text{.b}}=w{\text{.a}}\vee v{\text{.b}}=w{\text{.b}}))}$

この式を用いることで、式の中で使用されているすべての変数vとその型の列名aに対して、同様の式を追加することにより、安全でないクエリ式を同等の安全なクエリ式に書き換えることができます。これは実質的に、すべての変数がアクティブ ドメインの範囲を自由に動かせることを意味します。既に説明したように、表現されたクエリがドメインに依存しない場合は、意味論は変わりません。