基本テーブル、テーブル式、見出し推論

まず、タプル空間という言葉を定義する。A, B, Cなどが見出しだとする。見出しは名前集合の部分集合だが、名前集合にはドメイン割り当てが決まっていて、ドメイン集合も決まっている前提。

x, yなどはタプル集合とする。タプル集合はタプル空間の任意の部分集合のこと。ただし、すべての要素（タプル）が同じ見出しを持つとする。Heading(x) はタプル集合の見出し、A = Heading(x) であることを x::A と書く。

{t₁, ..., t_n} を基本テーブルの集合として、これらには見出しが決まっているとする。基本テーブルの全体をBasicとする。

1. 基本： t∈Basic ⇒ t::Heading(t)
2. 射影： x::A, B⊆A ⇒ x[B] :: B
3. 結合： x::A, y::B ⇒ x*y::A∪B' B'はBのAに対する自然リネーム

次に、x[X→Y] の形に式をタプル関連式と呼び、x[X→Y]::X→Y と書く。このとき

1. x::A X⊆A, Y⊆A ⇒ x[X→Y]::X→Y
2. 特に、x[X, X]::X→X
3. f::X→Y, g::Y→Z ⇒ f;g:X→Z

ρによる意味割り当て：

1. 基本： t∈Basic, t::A ⇒ 〚t〛 = ρ(t) ⊆Tuple(A)
2. 射影： x::A, B⊆A ⇒〚x[B]〛 = Proj_A→B(〚x〛)
3. 結合： x::A, y::B, C=A∩B' ⇒ 〚x*y〛 = {(s, t')∈Tuple(A)×Tuple(B') | s[C] = t'[C] }
4. x::A X⊆A, Y⊆A ⇒ 〚x[X→Y]〛 = {(s, t)∈Tuple(X)×Tuple(Y) | s[X]#t[Y]∈x}
5. f::X→Y, g::Y→Z ⇒ 〚f;g〛 = 〚f〛;〚g〛

正確には、〚-〛_ρ と書くべき。

テーブル式とテーブル関連式の全体は、圏となる。リネームによるクロスジョインを入れると、対称モノイド・ダガー圏になる。

基本割り当てρを拡張して、関係圏Relへの関手ができる。この関手ρ^~がデータベース状態を定義する。ρ^~ = 〚-〛_ρ。

述語から部分恒等を作って、拡張した圏（対象はそのまま）カロウビ展開圏を作る。カロウビ展開圏の射は、タプル空間とタプル空間上の述語の組。カロウビ展開圏では対象が増える。

できた圏：

• 対象は、タプル空間のdefinableな部分集合。
• 射は、タプル空間のあいだの関連（数学的二項関係）のコンパチな2つの対象の3つ組。

---

• 課題： タプル空間を対象とする関係圏とカロウビ展開圏のところが曖昧。はっきりさせる。