データベースの型理論と関係

• 型＝データ型＝集合
• 基本型＝基本データ型＝基本集合
• 直積型構成子
• 直積型＝直積データ型＝直積集合
• 直積型＝タプル型
• ペア型⊆タプル型
• ベキ集合型構成子＝ベキ型構成子
• { {ベキ集合}{型 | データ型} | {ベキ}{型 | データ型 | 集合} }
• {制約 | 制限}{_ | 条件} を使った型
• {制約 | 制限}型
• 基本的直積型 := 基本型を型引数にした直積型
• ベキ制限型 := ベキ型に制限を使った型

基本型（＝単純型＝プリミティブ型＝スカラー型）は事前に決める（例：bool, int, real, string, unit）。基本型に直積型構成子（＝直積集合構成子＝直積集合演算子＝直積演算子）とベキ型構成子（＝ベキ集合構成子）を適用して作った型が派生型（＝導出型＝複合（composite）型＝コンプレックス型）。

型の制約（＝制限）条件は次の形で書く。

• t{x|p(x)}

例：

• int{n | 0≦n ∧ n≦10}

要素を列挙してもよい。

• int{1, 2, 3, 4, 5}

ベキ制限型の例：

• Pow(int){X | X is finite}

述語は次の書き方を許す。

1. 自然言語・日本語： Xは有限集合
2. 自然言語・英語： X is a finite set
3. 略式英語： X is finite
4. 後置述語記号： X isFinite
5. 前置述語記号： isFinite(X)

他の制約（＝制限）の例

1. X isFinite
2. X containsZero ⇔ 0∈X
3. X isBounded100 ⇔ ∀n∈int.(n∈X ⇒ |n|≦100)

より複雑なベキ制限型の例：

• Pow(int){X | ∀n, m, k∈int.(n∈X ∧ m∈X ∧ n≦k ∧ k≦m ⇒ k∈X)}

述語を先に定義しておくと：

• predicate isContiguous(X:Pow(int)) := ∀n, m, k∈int.(n∈X ∧ m∈X ∧ n≦k ∧ k≦m ⇒ k∈X)

• Pow(int){X | X isContiguous}
• Pow(int){X | Xは隣接連続}

基本的直積型に対するベキ制限型の例：

• Pow(string×int){X | π₂|_X isInj}

制限条件（＝制約条件）を書き換えていくと：

• π₂|_X isInj
• isInj(π₂|_X)
• isInj(π₂|_X:X→int)
• ∀x, y∈string×int. (π₂|_X)(x) = (π₂|_X)(y) ⇒ x = y
• ∀x, y∈string×int. (x, y∈X ⇒ (x.2 = y.2 ⇒ x = y))
• ∀x, y∈X. (x.2 = y.2 ⇒ x = y)
• x, yがXの要素のとき、x.2 = x.2 ならば x = y である。
• 2つのXの要素に対して、第2成分が等しいならば2つの要素は等しい
• 2つのXのタプルに対して、第2属性が等しいならば2つのタプルは等しい

関係

関係の表現が多様

1. 直積集合の部分集合 → 圏Relまたは多圏MRelの定義そのもの
2. 述語 → 圏Pred
3. 同時単射な写像スパン（の同値類） →圏Span（＝Span(Set)）の定義そのもの
4. 多値関数 → 圏MultiVal

圏の同型・同値

1. Rel{f∈Mor | f isUnivalent} Partial
2. Span{s∈Mor | s isJointlyInj} Rel
3. Rel Multival Kl(Set, Pow)
4. Partial PtSet Kl(Set, Maybe)
5. Pred MRel

注目すべき圏

1. Set
2. Partial （Set⊆Partial）
3. MultiVal（Set⊆Partial⊆MultiVal）
4. PtSet （PtSet Partial）
5. Rel （Rel MultiVal）
6. Pred （Pred MRel）
7. Span （Rel⊆Span)