路径合取查询、约束和视图的等式追逐

### 路径合取查询、约束和视图的等式追逐 在数据库查询和约束处理中，我们常常需要处理复杂的查询和约束关系。本文将介绍一种处理路径合取查询、约束和视图的方法，通过等式追逐的方式来解决相关问题。 #### 等式追逐示例 首先，我们来看一个等式追逐的示例。通过对(INV1)进行两次追逐，接着对(KEY2)和(KEY1)进行追逐，(FD - RETRO)被转换为如下形式： ```plaintext ∀(p ∈Proj) ∀(d ∈depts) ∀(s ∈d.DProjs) ∀(p′ ∈Proj) ∀(d′ ∈depts) ∀(s′ ∈d.DProjs) s = p.PName ∧p.PDept = d.DName ∧ s′ = p′.PName ∧p′.PDept = d′.DName ∧ p.PName = p′.PName ∧p = p′ ∧ d = d′ ⇒ d.MgrName = d′.MgrName ``` 这个约束(TRIV)在所有实例中都成立，无论其他约束如何。因此，(FD - RETRO)可以从(INV1, KEY2, KEY1)推导得出。 #### CoDi框架概述 为了更深入地解决这类问题，我们引入了CoDi框架。CoDi是一种语言和等式理论，它结合了字典处理和之前在集合与聚合方面的工作，使用了单子理论。 - **主要构造**： - **BigU**：`BigU (x ∈S) R(x) = ⋃_{i = 1}^{n} R(ai)`，用于集合的并操作。 - **All**：`All (x ∈S) B(x) = ⋀_{i = 1}^{n} B(ai)`，用于布尔表达式的合取。 - **Some**：`Some (x ∈S) B(x) = ⋁_{i = 1}^{n} B(ai)`，用于布尔表达式的析取。 我们使用通用符号`Loop`来表示`BigU`、`All`或`Some`，并常考虑以下形式的表达式： ```plaintext Loop (x ∈S) if B(x) then E(x) ``` 它是以下表达式的缩写： ```plaintext Loop(x1 ∈S1) · · · Loop(xn ∈Sn(x1, . . . , xn−1)) if B(x1, . . . , xn) then E(x1, . . . , xn) else null ``` 其中，`null`在`BigU`中表示空集，在`All`中表示`true`，在`Some`中表示`false`。我们还使用`sng E`表示单元素集合，以及`eq(E1, E2)`进行相等性测试和布尔合取。 - **字典**：我们用`σ ×> τ`表示字典类型，其中`σ`是键的类型，`τ`是条目的类型。`dom M`表示字典`M`的键集，`K ! M`表示字典`M`中对应键`K`的条目。 #### CoDi中的等价定律 CoDi有一些基本的等价定律，如下表所示： | 定律名称 | 定律内容 | | ---- | ---- | | (sng) | `BigU (x ∈S) sng(x) = S` | | (monad - β) | `Loop (x ∈sng(E)) E′(x) = E′(E)` | | (assoc) | `Loop (x ∈(BigU (y ∈R) S(y))) E(x) = Loop (y ∈R) (Loop (x ∈S(y)) E(x))` | | (null) | `Loop (x ∈empty) E(x) = null` | | (cond - loop) | `Loop (x ∈S) if B then E(x) = if B then Loop (x ∈S) E(x)` | | (commute) | `Loop (x ∈R) Loop (y ∈S) E(x, y