表示独立性

形式陈述 ​

设一个抽象数据类型公理库抽象数据类型Abstract data type · ADT由值集合与操作语义定义、独立于具体表示的数据接口。的接口依赖隐藏表示类型，写成 $I(Rep)$。两个实现分别选择 $Re{p}_1,Re{p}_2$ 并打包为

$$M_1=\mathsf{pack}[Re{p}_1,m_1],M_2=\mathsf{pack}[Re{p}_2,m_2]$$

，二者都有存在类型公理库存在类型Existential type · Existentially quantified type隐藏一个见证类型及其实现值，只允许客户端通过公开接口使用该表示的量化类型。 $\mathrm{\exists }Rep.I(Rep)$。表示独立性不从“类型相同”直接得出；还需给出抽象关系

$$R\subseteq \mathsf{Val}(Re{p}_1)\times \mathsf{Val}(Re{p}_2)$$

并证明接口的每个组成部分保持它。若接口含初始值、更新与观察操作，典型义务是

$$({\mathsf{empty}}_1,{\mathsf{empty}}_2)\in R,$$$$(r_1,r_2)\in R⟹({\mathsf{insert}}_1(a,r_1),{\mathsf{insert}}_2(a,r_2))\in R,$$

以及

$$(r_1,r_2)\in R⟹{\mathsf{member}}_1(a,r_1)={\mathsf{member}}_2(a,r_2).$$

函数参数、结果、积与其他接口类型都要按相应逻辑关系逐层提升。只比较某次操作的返回值不够；更新后的表示仍在 $R$ 中，才保证后续任意长的客户端调用序列继续相关。

令 $C[-]$ 是只通过该存在接口使用模块、最终产生可观察类型 $O$ 的任意良类型客户端上下文。若 $M_1,M_2$ 在存在类型的关系解释下相关，且 $O$ 的基关系就是所关心的观察等价，则

$$\mathrm{Obs}(C[M_1])=\mathrm{Obs}(C[M_2]).$$

证明桥梁分三步：先选 $R$，再验证两个实现值在 $I(Rep)$ 的关系解释下相关，最后把客户端视作带一个模块变量的开放项，应用逻辑关系基本定理公理库逻辑关系基本定理Fundamental theorem of logical relations · Fundamental lemma良类型项在点对点相关的环境替换下产生逻辑相关结果的核心引理。。基本定理保证良类型客户端保持关系；从结果相关到观察相同还要使用所选逻辑关系的 adequacy，不能把两步压成一句未经说明的“封装即可替换”。

直觉 ​

接口像一面只开了若干窗口的墙。两个实现背后的房间布局可以完全不同，客户端却只能从窗口递交请求、接收结果。表示关系不是要求两边内部状态长得一样，而是给出“这两个不同状态表达同一个抽象状态”的对应方式。

每个接口操作都必须把这条对应关系接续下去。初始值把两边放到同一个起点，更新操作维护对应，观察操作给出相同外部答案；于是客户端无论怎样组合这些操作，都没有机会走到关系之外。

例子与边界 ​

集合接口提供 empty、insert 与 member。实现一用保持有序且无重复的列表 $L$，实现二用平衡搜索树 $T$。定义

$$R(L,T)⟺\mathrm{elements}(L)=\mathrm{elements}(T)$$

，等号比较两边表示的数学集合。空列表与空树相关；向相关表示插入同一元素后，二者仍表示同一集合；对相关表示查询同一元素，member 返回相同布尔值。因此只使用这三个操作的客户端无法分辨收到的是列表包还是树包。

若接口新增 iterate 并承诺具体遍历顺序，集合相等已不足以保证结果相关：有序列表可能升序输出，树实现的遍历策略则可能不同。若接口暴露地址身份、内部节点、异常种类、终止行为或运行时间，这些也会进入可观察集合；要么加强 $R$ 与操作义务，要么放弃原来的不可区分结论。性能只有明确写入规格时才属于表示独立性要保持的观察。

带局部可变状态的模块还会分配地址，并在后续调用中扩展堆关系。此时常用 Kripke possible worlds 记录两边位置的持续对应，用 step index 处理递归状态与高阶存储；朴素的静态 $R\subseteq Re{p}_1\times Re{p}_2$ 无法独自描述新分配、隐藏别名和未来更新。

推论与应用 ​

表示独立性支撑模块替换、数据结构重构和编译器表示优化。客户端证明只依赖抽象接口，维护者便可更换内部结构而不重做全部客户端证明；需要重证的是新旧实现满足同一关系义务。

存在类型负责隐藏 witness，表示独立性负责证明隐藏后的行为保证。两者缺一不可：没有类型封装，客户端可能直接检查表示；只有封装没有关系证明，一个错误实现也能满足表面签名，却不满足抽象行为。

参考资料

• John C. Mitchell and Gordon D. Plotkin, “Abstract Types Have Existential Type,” ACM TOPLAS 10(3), 1988。
• John C. Reynolds, “Types, Abstraction and Parametric Polymorphism,” in Information Processing 83, 1983，relational account of data abstraction。
• Andrew M. Pitts and Ian D. B. Stark, “Operational Reasoning for Functions with Local State,” in Higher Order Operational Techniques in Semantics, Cambridge University Press, 1998。