CHAPTER 3 Data Abstraction

Algebraic Interfaces for Abstract Data Types

举队列为例，在一般编程中，我们构造出数据结构就 ok 了。但是如果我们要遵照形式化正确证明，我们还要补充一个规则集合，并用 data type 的操作量化。还是讲队列，需要满足两条：

\[dequeue(empty) = \cdot\]

\[\forall q.dequeue(q) = \cdot \Rightarrow q = empty\]

给出两个比较明显的实现：

• enqueue to list fronts and dequeue from listbacks
• enqueue to list backs and dequeuefrom list fronts

上述两个实现不够效率，这里有一个著名的，更聪明的实现，它实现了平摊常数时间(线性时间覆盖整个操作序列)，但是我们需要扩展我们的代数风格来适应它。

Algebraic Interfaces with Custom Equivalence Relations

我们发现用一个新的数学操作来扩展队列的基本接口是很有用的。

引入等价关系（自反，对称，传递）

Here is its implementation, relying on list-reversal function rev？？

双 list 实现队列，不够时反转添加至弹出 stack，形式化等价的证明。

\[rep((l_1,l_2)) = l_1 \bowtie rev(l_2)\]

\[q_1 \approx q_1 = rep(q_1) = rep(q_2)\]

为什么我们需要经历引入自定义等价语句的麻烦呢？思考后面的等价问题。一个为\(([],[2])\)一个为\(([2],[])\)。这个数据结构是不规范的，因为相同的逻辑值可能有多个物理表示。等价关系让我们指出哪些物理表示是等价的。

Representation Functions

基于representation functions风格的表示方法。我们可以强制。只要存在任何兼容的函数就足以显示队列实现的正确性，而且这种方法基本上可以将所有其他数据结构转换为抽象数据类型。

感觉就是把具备的性质用rep()表示出来。

修正队列的类型定义

修正的 Axiom（公理）

Fixing Parameter Types for Abstract Data Types

这是另一种经典的抽象数据类型：有限集（finite sets），我们在这里写布尔集合。

\[ \begin{aligned} t(a) & \quad : \quad Set \\ empty & \quad : \quad t(a) \\ add & \quad : \quad t(a) \times a \rightarrow t(a) \\ member & \quad : \quad t(a) \times a \rightarrow \mathbb{B} \end{aligned} \]

一种简单的实现方法是使用 data type unsorted lists。

我们可以为特定的元素类型和使用模式构建专门的有限集。对于仅构建连续数字集的工作负载，此实现可能比基于泛型列表的实现快得多，它将次方转换为线性时间复杂度。！！给了一个 Range。