计算充分性

把程序解释成数学函数并不自动保证数学结果可由执行得到。证明需要把两边接起来。形式近似关系让一个语义元素携带一条可执行承诺：布尔非底元素承诺实际得到那个值，函数元素则承诺每个已经符合输入承诺的程序都产生符合输出承诺的应用。

底元容纳所有尚未取得结果的计算。守卫指称为底时，整个条件式的语义也是底；形式近似因此在这个分支直接成立。这正是证明里必须同时处理基类型底元与函数类型底元的原因。

形式近似及两个辅助事实 ​

对 $d\in D_A$ 与闭项 $e:A$，递归定义 $d{◃}_{A}e$：

输入 $u$ 遍历所有闭项，包含发散项；传名求值把尚未求值的实参代入函数体，因此环境关系也使用闭项替换。

先按类型证明底元近似任意项。Bool 情形来自定义；箭头情形任取 $a{◃}_{A}u$，有 ${\mathrm{\perp }}_{A\to B}(a)={\mathrm{\perp }}_B$，类型归纳假设给出 ${\mathrm{\perp }}_B{◃}_{B}eu$，故满足箭头分支。

再证明有限求值不改变近似关系：若 $e{\to }^{\ast }{e}^{\prime }$，则 $d{◃}_{A}e⟺d{◃}_A{e}^{\prime }$。Bool 处，确定性说明有限前缀之前与之后能到达的布尔值相同；箭头处，对任何闭实参 $u$，函数位置规则给出 $eu{\to }^{\ast }{e}^{\prime }u$，应用结果类型 $B$ 上的归纳假设即可。这个事实同时允许从 β 收缩后的函数体倒推到应用项，以及从选出的条件分支倒推到整个条件式。

基本引理的完整归纳 ​

设 $\mathrm{\Gamma }⊢e:A$，$\rho$ 是语义环境，$\sigma$ 把每个 $x:B\in \mathrm{\Gamma }$ 替换为闭项 $\sigma (x):B$，并满足 $\rho (x){◃}_B\sigma (x)$。要证

这是逻辑关系基本定理公理库逻辑关系基本定理Fundamental theorem of logical relations · Fundamental lemma良类型项在点对点相关的环境替换下产生逻辑相关结果的核心引理。在本语言里的具体实例。证明按类型推导归纳，各种构造如下。

1. 变量。 $e=x$ 时，左边为 $\rho (x)$，右边为 $\sigma (x)$，正是环境假设。
2. 布尔常量。 true 和 false 均零步求值到自己，满足各自的非底近似条件。
3. 发散常量。 $[[\mathrm{\Omega }]]=\mathrm{\perp }$，由底元引理得 $\mathrm{\perp }{◃}_{\mathsf{Bool}}\mathrm{\Omega }$。
4. 应用。 若 $e=rs$，归纳假设给出 $[[r]]\rho {◃}_{B\to A}r[\sigma ]$ 和 $[[s]]\rho {◃}_{B}s[\sigma ]$。把后一对输入交给前一箭头关系，得到 $[[r]]\rho ([[s]]\rho ){◃}_{A}r[\sigma ]s[\sigma ]$，即所求。
5. 抽象。 若 $e=\lambda x:B.r$，为证明箭头分支，任取 $a{◃}_{B}u$。先把绑定变量改名，使它不与替换冲突，再扩展环境为 $\rho [x\mapsto a]$、替换为 $\sigma [x\mapsto u]$。函数体归纳假设给出 $[[r]](\rho [x\mapsto a]){◃}_{A}r[\sigma [x\mapsto u]]$。后者正是 $(\lambda x:B.r[\sigma ])u$ 的 β 收缩结果；有限求值闭包把结论搬回应用项，完成箭头条件。
6. 条件式。 设 $e=\mathsf{if}g\mathsf{then}r\mathsf{else}s:A$。若 $[[g]]\rho =\mathrm{\perp }$，严格条件解释给出 $[[e]]\rho ={\mathrm{\perp }}_A$，底元引理立即适用，即使 $A$ 是函数类型也成立。若守卫指称为 $T$，守卫的 Bool 近似给出 $g[\sigma ]\Downarrow \mathsf{true}$；整个条件式因此有限步进入 $r[\sigma ]$。分支归纳假设给出 $[[r]]\rho {◃}_{A}r[\sigma ]$，有限求值闭包给出所求。$F$ 情形同理选择 $s[\sigma ]$。

以上覆盖 $L$ 的全部类型规则。对闭项取空环境和空替换，再在 Bool 处展开 $◃$，便得到计算充分性。若进一步加入一般递归，类型规则会增加不动点分支，证明也需相应处理极限闭包。

另一方向为什么成立 ​

求值可靠性来自语义替换等式

该式按 $e$ 的结构归纳：变量分成 $x$ 与其他变量；应用、条件式把子项等式代入解释式；抽象先改名避免捕获，再对每个语义实参使用函数体归纳假设；常量不依赖替换。于是 β 根步保持指称；两个条件根步由选择语义直接保持；$\mathrm{\Omega }$ 自环也保持。组合性把根步等式提升到每个 $E$ 中，有限步到布尔常量便给出可靠性。

例如 $p=(\lambda x:\mathsf{Bool}.\mathsf{true})\mathrm{\Omega }$ 的指称为 $T$，实际一步得到 true；$q=\mathsf{if}\mathrm{\Omega }\mathsf{then}\mathsf{true}\mathsf{else}\mathsf{true}$ 的指称为 $\mathrm{\perp }$，实际永远困在守卫。相同的两个分支不足以消除严格守卫。

设同型闭项 $e,e^{\prime }$ 指称相等。对任意闭合 Bool 程序上下文 $C$，组合性先给出 $[[C[e]]]=[[C[e^{\prime }]]]$，本页的观察对应再给出 $\mathrm{Obs}(C[e])=\mathrm{Obs}(C[e^{\prime }])$。因此

这是模型的上下文可靠性，与前面的“有限求值保持指称”是不同陈述。组合性负责把部件相等传到完整程序，求值可靠性与计算充分性再把完整程序的指称翻译成实际观察。

验收时应能亲手补出应用、抽象和函数结果条件式的三段归纳，并指出最后推论用了哪条组合等式。反方向 $e{\simeq }_{\mathrm{ctx}}{e}^{\prime }\Rightarrow [[e]]=[[e^{\prime }]]$ 仍可能失败；完全抽象公理库完全抽象Full abstraction · 全抽象比较语义相等与上下文等价的双向对应，并用三个布尔探针证明充分模型仍可区分语言无法观察的差异。给出同一语言、同一模型中的明确反例。