表示独立性

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

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

固定一个纯计数器接口和客户端语言 ​

先把一般结论落实到一个能逐条证明的模型。接口为

三个分量依次命名为 zero、read、inc；三元组是嵌套积的记法。计数器状态是不可变值，inc 返回一个新状态，客户端可以保留旧状态。本例不观察地址、时间或分配，也不含可变引用、异常、一般 fix 或按隐藏类型分支的操作。

客户端在最外层打开一次包，得到新鲜抽象类型 $\alpha$ 和 $m:I(\alpha )$。包内客户端的类型为

项包括变量、λ/应用、二元积/投影、$()$、true/false、条件式、自然数零/后继，以及任意结果类型的原始递归；let 是 λ 应用的语法糖。采用纯传值求值理路传值调用Call by value · CBV仅当实参先求值为值后才进行函数体替换的求值策略。：先求函数与参数，再代入参数值；积的两个分量均求成值；条件式只求选中分支。客户端不能把 $\alpha$ 当 Nat 做递归，也没有直接比较两个 $\alpha$ 值的内建规则。

为使递归的终止与归纳义务明确，规定

先求 $t\Downarrow \overline{k}$，再执行下述辅助求值 ${\mathrm{Rec}}_A(k,z,i,y.s)$：$k=0$ 时求 $z$；$k=j+1$ 时，先将 ${\mathrm{Rec}}_A(j,z,i,y.s)$ 求成值 $w$，然后求 $s[\overline{j}/i,w/y]$。这里累积结果先求值，再代入步进项，是本页明确选择的严格递归语义。$A$ 可以为 $\alpha$ 或函数类型，不局限于 Nat。[3]

最终客户端返回 Nat，故 $\alpha$ 不出现在公开结果类型中，满足存在消去的非逃逸条件。这个边界量化的是上述片段内的所有良类型客户端；带状态或不终止的扩充需要新的计算关系。

两个实现与三项关系义务 ​

第一个包用自然数表示状态：

第二个包用有限单位列表表示状态：

列表构造及消去只用于私有实现。其观察函数由 $\mathsf{length}([])=0$、$\mathsf{length}(()::xs)=\mathsf{succ}(\mathsf{length}(xs))$ 定义，沿有限列表长度递减，必定终止。客户端打开包后只知道 $\alpha$，不会获得把它当列表匹配的类型规则。

选关系

现在逐项核验，而不是从相同签名推断行为相同。

1. 初值满足 $R(0,[])$。
2. 若 $R(\overline{n},xs)$，两个 read 都返回 $\overline{n}$。
3. 若 $R(\overline{n},xs)$，则 $n+1=\mathrm{length}(()::xs)$，所以两个 inc 返回的值仍在 $R$ 中。

这些等式对全部自然数和有限单位列表成立，已经覆盖所有关系中的状态，而非只覆盖某张执行表。

从接口关系证明任意客户端 ​

按客户端类型提升表示关系 ​

令 ${\theta }_N(\alpha )=\mathsf{Nat}$、${\theta }_L(\alpha )=\mathsf{List}(\mathsf{Unit})$。关系 ${\mathcal{V}}_R[A]$ 比较类型分别为 $A[{\theta }_N]$、$A[{\theta }_L]$ 的闭值。定义

Bool 取同一布尔值，Unit 只有 $((),())$，积按分量相关；计算关系为

箭头分支要求

这里输入只需相关，通常并不具有相同具体类型或语法。定义按客户端类型表达式 $A$ 递归；遇到 $\alpha$ 直接使用 $R$，不会继续展开具体列表类型，因此没有循环定义。[1][2]

开放项基本引理及全部构造 ​

对所有 $\alpha \mathsf{type};\mathrm{\Gamma }⊢e:A$，若两个闭值替换 ${\sigma }_N,{\sigma }_L$ 对 $\mathrm{\Gamma }$ 的每个变量都给出 ${\mathcal{V}}_R$ 相关值，则

必须对整个环境作此陈述，才能在 λ 和递归绑定器下使用归纳假设。按类型推导归纳：

• 变量和常量。 变量用环境分量；零、Unit、布尔常量分别返回相关值；后继先由子项归纳得到相同自然数，再在两侧同时加一。
• 积和投影。 两个子项各自终止到相关分量，传值积构造返回相关积；投影从相关积取相同位置，得到对应分量。
• 抽象。 λ 已是值。任取相关参数值，将它们加入两套相关替换；函数体归纳假设给出相关且终止的结果，再由传值 β 求值规则得到箭头条件。
• 应用。 函数项与参数项的归纳假设分别提供相关函数值和相关参数值；把后一对交给箭头关系，得到两次调用的相关结果。求值前缀再接回完整应用。
• 条件式。 守卫归纳给出同一布尔值，故两边进入同一侧分支；该分支归纳给出结果。不要求两侧私有表示相等。
• 原始递归。 对 $t$ 的归纳给出同一 $\overline{k}$。再对辅助求值的自然数 $k$ 作归纳：零时用基础项 $z$ 的类型推导归纳假设；$k=j+1$ 时，先由数值归纳得到相关累积值 $w_N,w_L$，再把相同前驱 $\overline{j}$ 和这对累积值加入环境，对步进项 $s$ 使用类型推导归纳假设。它同时保证本轮终止和结果相关，即使 $A$ 是 $\alpha$ 或箭头也成立。

这些是本页客户端文法的全部构造，let 随 λ/应用得到。有限列表的私有递归不属于客户端归纳；它的终止和 read 保持关系已经单独核验。

三项接口义务正好说明两个实现三元组在 ${\mathcal{V}}_R[I(\alpha )]$ 中相关。于是把基本引理专门化到 $\mathrm{\Gamma }=m:I(\alpha )$、$A=\mathsf{Nat}$，得到任意允许客户端在两种实现下都终止到同一个数字。最外层 unpack 的消去规则只负责把两种 witness 和实现值分别代入。由 ${\mathcal{E}}_R[\mathsf{Nat}]$ 的定义，结果相关已经意味着实际观察相同：

这次从逻辑关系到观察的充分性是直接展开定义，无须借用传名、含发散语言中的另一份计算充分性定理。

高阶调用、分支和保留旧状态的账本 ​

下面代码中的三元组展开是积投影的缩写，数字是零和后继的缩写。另定义 $\mathsf{iszero}(n)={\mathrm{rec}}_{\mathsf{Bool}}(n;\mathsf{true};i,y.\mathsf{false})$，$\mathsf{add}(a,b)={\mathrm{rec}}_{\mathsf{Nat}}(a;b;i,y.\mathsf{succ}(y))$。

unpack [α, m] = M in
let (zero, read, inc) = m in
let saved : α = inc zero in
let iterate : Nat → (α → α) → α → α =
  λk:Nat. λf:α→α. λx:α. recα(k; x; i,y. f y)
in
let chosen : α → α =
  if iszero (read saved) then inc else λx:α. inc (inc x)
in
let later : α = iterate (succ (read saved)) chosen saved in
add (read later) (read saved)

read saved 为 $1$，所以两边选择双增量函数，迭代次数为 $2$。用 $[(){]}^n$ 表示含 $n$ 个单位值的列表：

最终两边都返回 $5+1=6$。保存旧值和高阶调用都在证明范围内；只证明“一次inc返回同一个数字”尚不足以覆盖这个客户端。

同一签名下仍能放入错误实现 ​

令 $M_{\mathrm{bad}}$ 仍用 Nat，但把 inc 改为 $n\mapsto n+2$，其余两项不变。它仍具有 $\mathsf{Counter}$ 类型。客户端 unpack [α,m]=M in let (zero,read,inc)=m in read (inc zero) 却分别观察到正确包的 $1$ 与错误包的 $2$。

对照列表实现，从相关初值 $R(0,[])$ 出发，错误更新产生 $2$ 与 $[()]$，不再满足 $R$。签名检查通过，表示关系的更新义务失败，区分客户端便有了入口。若把时间或可变地址也加入观察，虽然两份正确实现的数值证明保持成立，原来的不可区分结论仍需扩充其观察关系。

其他接口与局部状态的边界 ​

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

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

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

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

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

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