完全抽象

函数域中可能存在某个数学输入，而源语言没有程序能实现它。模型可以用这个额外输入区分两个高阶程序；实际客户端却只能编写语言允许的输入，因而可能永远看不见差别。

仅说“存在不可定义函数”还不够：必须找到两个源程序，证明所有源上下文都无法区分它们，再用那个数学输入算出不同结果。下面分三步完成这三个量词不同的任务。

两个只在通过全部探针后才不同的程序 ​

令 $H=\mathsf{Bool}\to \mathsf{Bool}\to \mathsf{Bool}$。对 $b\in \{\mathsf{true},\mathsf{false}\}$ 定义闭项 $T_b:H\to \mathsf{Bool}$：

T_b = λf:H.
  if f true Omega then
    if f Omega true then
      if f false false then Omega else b
    else Omega
  else Omega

代码中的 Omega 就是 $L$ 的常量 $\mathrm{\Omega }$。三次应用的类型均为 Bool，所有条件分支也都是 Bool，所以整个项具有所标类型。到达最后的 $b$ 必须依次通过

某个守卫发散，计算就停留在那里；得到与要求相反的布尔值，则走向显式 $\mathrm{\Omega }$。两项的唯一语法差别藏在通过全部探针之后。

三元关系证明没有源程序通过探针 ​

在 $D_{\mathsf{Bool}}$ 上定义三元关系

递归定义 $R_{A\to B}(f_1,f_2,f_3)$：对每个满足 $R_A(a_1,a_2,a_3)$ 的输入三元组，都有 $R_B(f_1(a_1),f_2(a_2),f_3(a_3))$。先证明一个后面要用的底元事实：任何第一或第二分量为 ${\mathrm{\perp }}_A$ 的三元组均满足 $R_A$。Bool 处直接成立；箭头处应用于相关输入后，对应输出仍是 ${\mathrm{\perp }}_B$，由结果类型上的归纳假设成立。

现在证明 $L$ 的每个构造保持这族关系。更准确地，若三个语义环境逐变量相关，则同一良类型项在三个环境中的解释相关。对类型推导归纳如下。

• 变量直接取环境分量；true、false 的对角三元组满足基关系；$\mathrm{\Omega }$ 的三元组为 $(\mathrm{\perp },\mathrm{\perp },\mathrm{\perp })$。
• 应用把相关函数三元组作用在相关实参三元组上，结论正是箭头关系的定义。
• 抽象任取相关实参三元组，分别扩展三个环境，在函数体上使用归纳假设，得到箭头关系。
• 条件式的三个守卫相关。若第一或第二守卫为底，则同一分量的整个条件解释为结果类型的底，前述底元事实给出结果相关；否则基关系强迫三个守卫为同一个布尔值，于是三个解释选择同一侧分支，分支归纳假设给出结果相关。这里覆盖了结果为函数的条件式，不能只核查 Bool 结果。

这些正是基本定理公理库逻辑关系基本定理Fundamental theorem of logical relations · Fundamental lemma良类型项在点对点相关的环境替换下产生逻辑相关结果的核心引理。的全部构造义务。取空环境，任何闭项 $f:H$ 的解释 $h=[[f]]$ 都满足 $R_H(h,h,h)$。由于

连续应用两次箭头关系得到

可是 $(T,T,F)$ 不满足这个关系。因此没有闭合 $L$ 项能使三个语义探针分别为 $T,T,F$。若操作探针 (1) 都成功，求值可靠性就会给出这个不可能的语义三元组。故对每个闭项 $f:H$，$T_{\mathsf{true}}f$ 与 $T_{\mathsf{false}}f$ 均发散。

从所有实参提升到所有程序上下文 ​

接下来把调用结果的结论传到任意程序位置，包括 λ 体和高阶参数。为此定义闭项上的二元传名关系 ${\mathcal{Q}}_A$：

这里两边输入可以不同，也可以不是值。先记两条按类型归纳的闭包。其一，对任意一侧作有限弱求值，不改变 ${\mathcal{Q}}_A$：Bool 处有限前缀不改变观察；箭头处把前缀放到函数位置，对结果类型归纳。其二，两个都不能求值到任何值的闭项，在每个类型 $A$ 都相关：Bool 处都是发散；箭头处它们应用于任意参数时，仍须先计算永远不能完成的函数位置，故应用也都不能到达值，再对结果类型归纳。

证明环境版本：若 $\mathrm{\Gamma }⊢e:A$，两个闭项替换 $\sigma ,\tau$ 对每个变量给出 $\mathcal{Q}$ 相关项，则 $e[\sigma ]{\mathcal{Q}}_{A}e[\tau ]$。变量取环境条件；布尔常量观察相同；$\mathrm{\Omega }$ 两侧都发散。应用直接使用箭头条件。抽象任取 ${\mathcal{Q}}_B$ 相关的闭实参 $u,v$，将它们加入两个替换，对函数体用归纳假设，再用有限 β 求值闭包搬回两个应用。条件式由守卫归纳假设得到相同的 Bool 观察：若都是 $T$ 或都是 $F$，两边有限步进入同一侧的相关分支；若都是发散，两个条件式都不能成为值，由第二条闭包得到任意结果类型上的相关性。至此覆盖全部类型规则。

最后，对任意上下文 $C:A\Rightarrow \mathsf{Bool}$，把洞换成一个新自由变量 $z:A$，得到 $z:A⊢C[z]:\mathsf{Bool}$。若 $e{\mathcal{Q}}_A{e}^{\prime }$，对替换 $z\mapsto e$、$z\mapsto e^{\prime }$ 使用刚证明的环境引理，得到 $C[e]{\mathcal{Q}}_{\mathsf{Bool}}C[e^{\prime }]$，即观察相同。这明确覆盖所有良类型单洞上下文。

对我们的一对 $T$ 项，任意相关的 $u,v:H$ 都是闭合 $L$ 项；上一节已经证明 $T_{\mathsf{true}}u$ 与 $T_{\mathsf{false}}v$ 均发散，故它们在 Bool 处相关。箭头定义因此给出两个 $T$ 项相关，再由上下文引理得到

模型中的九格输入却能区分它们 ​

模型允许如下柯里化函数 $\mathrm{por}\in D_H$。行是第一个参数，列是第二个参数：

其规则是：只要任一参数为 $T$ 就返回 $T$；两个均为 $F$ 才返回 $F$；其余情况为底。检查单调性只需把任一坐标的底提升为 $T$ 或 $F$。原结果若为底，提升后任何结果都在它上方；原结果若为 $T$，已经存在一个 $T$ 坐标，提升另一个底不会消除它；原结果若为 $F$，两个坐标已是 $F$，没有严格向上的提升。这覆盖九格的全部可比输入。各类型域有限，单调即 Scott 连续，所以表确实定义了模型中的合法元素。

依次查表可得

代入 $T_b$ 的解释，外层两个条件都进入 then，内层进入 else，于是

两指称是函数，在同一输入上结果不同，故不相等。结合 (2)，得到一个计算充分、上下文可靠、但不完全抽象的模型。三元关系还已经证明 por 不可由 $L$ 项定义；因此 $[]\mathrm{por}$ 不是合法 $L$ 程序上下文。por 属于数学模型，正是它使模型比源程序的观察更细。

本单元可以用三个问题验收。第一，常返回 true 的函数与严格读取布尔参数后返回 true 的函数，被 $[]\mathrm{\Omega }$ 区分，答案为 $T$ 与发散；这不是完全抽象反例，因为语义与上下文两边都不同。第二，语义相等推出上下文等价，依靠组合性和基类型充分性。第三，本页的 $T$ 对在所有 $L$ 上下文中相同，却在数学输入 por 上分别为 $T,F$，因此失败的是完全抽象的反方向。九格表只验证那个输入；覆盖所有程序与所有上下文的工作分别由三元、二元基本引理承担。

编译阶段的语义保持公理库语义保持的编译器阶段Semantics-preserving compiler pass · Correct compiler transformation · 编译阶段语义保持在固定观察、错误与未定义行为契约下，要求一次编译变换的目标程序不产生源程序未允许的行为。还有另一种完全抽象问题。若翻译 $K:S\to T$ 保持接口类型，翻译的完全抽象要求

两边分别量化源语言与目标语言的全部允许上下文，并使用各自声明的观察。完整闭程序运行结果保持，只涉及已经链接好的程序；翻译的完全抽象还要求分析任意目标客户端能否区分源语言中等价的部件。前者比较完整执行，后者比较两种语言中的部件等价，而指称模型的完全抽象比较程序等价与数学对象相等。