上下文等价 | Codeboy's Blog

形式陈述

先固定语言和观察

两个程序在一次测试中给出相同结果，是否就能在任何客户端中互换？上下文等价把“任何客户端”变成一个明确的量词。本页及后续充分性、完全抽象单元始终使用同一小语言 $L$ ：简单类型 λ 演算的布尔扩充，采用弱传名调用，并额外加入一个发散常量。具体语法为

\begin{aligned} A,B&::=\mathsf{Bool}\mid A\to B,\\ e&::=x\mid\lambda x:A.e\mid e\,e\mid\mathsf{true}\mid\mathsf{false} \mid\mathsf{if}\ e\ \mathsf{then}\ e\ \mathsf{else}\ e\mid\Omega. \end{aligned}

变量、抽象、应用使用通常的简单类型规则； $\mathsf{true},\mathsf{false},\Omega:\mathsf{Bool}$ ，条件式的守卫必须为 Bool，两个分支必须具有同一类型 $A$ ，整个条件式也为 $A$ 。这里的 $\Omega$ 是新增的带类型常量，规则为 $\Omega\to\Omega$ ；它不是无类型自应用项的缩写。纯 STLC 的强正规化定理因这个新增规则而不再适用。

值为布尔常量和 λ 抽象。根收缩规则是

(\lambda x:A.e)u\mapsto e[u/x],\qquad \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ u\ \mathsf{else}\ v\mapsto u,

以及 false 选择 $v$ 的规则和 $\Omega\mapsto\Omega$ 。替换避免捕获。完整求值仅在

E::=[\ ]\mid E\,e\mid\mathsf{if}\ E\ \mathsf{then}\ e_1\ \mathsf{else}\ e_2

中收缩： $E[r]\to E[r']$ 。不预先计算实参，不进入尚未调用的 λ 体。写 $p\Downarrow b$ 表示有限步到达布尔值 $b$ 。闭合良类型项满足保持与进展：变量情形被闭合性排除；应用先处理函数位置，函数值必为 λ；条件守卫的值必为布尔； $\Omega$ 总能再走一步。每种非值形状又只指定一个下一步，所以求值确定，闭合 Bool 程序的观察恰有三种：

\operatorname{Obs}(p)= \begin{cases} T,&p\Downarrow\mathsf{true},\\ F,&p\Downarrow\mathsf{false},\\ \bot,&p\text{ 有无限求值序列}. \end{cases}

$\bot$ 是发散观察，不是语言中的第三个布尔值。本单元不观察步数、内存、异常或副作用，语言也没有这些构造。

量化全部程序上下文

单洞程序上下文允许洞出现在任意语法位置：

\begin{aligned} C::={}&[\ ]\mid\lambda x:A.C\mid C\,e\mid e\,C\\ &\mid\mathsf{if}\ C\ \mathsf{then}\ e\ \mathsf{else}\ e\\ &\mid\mathsf{if}\ e\ \mathsf{then}\ C\ \mathsf{else}\ e\\ &\mid\mathsf{if}\ e\ \mathsf{then}\ e\ \mathsf{else}\ C. \end{aligned}

洞恰出现一次；洞外的 $e$ 可以含由外层绑定器约束的变量。记 $\vdash C:A\Rightarrow\mathsf{Bool}$ ，意为把洞临时当作一个具有类型 $A$ 的新常量后，整个表达式能在空环境中定型为 Bool。填入闭项不会发生自由变量捕获。对闭项 $e,e':A$ ，定义

e\simeq_{\mathrm{ctx}}e' \iff \forall C\ (\vdash C:A\Rightarrow\mathsf{Bool} \Longrightarrow\operatorname{Obs}(C[e])=\operatorname{Obs}(C[e'])).

程序上下文 $C$ 与求值上下文 $E$ 的职责不同。例如 $(\lambda x:\mathsf{Bool}.[\ ])\,\mathsf{true}$ 是可观察 Bool 洞的程序上下文，洞在 λ 体内，故不是允许下一步在洞中收缩的 $E$ 。定义中的量词覆盖这些任意位置，求值规则则只沿 $E$ 指定的位置执行。

直觉

类型规定客户端能怎样使用部件；观察规定使用后什么差异值得区分；上下文量词则覆盖所有满足接口的使用方式。函数本身已经是值，只看它“能否求值到函数”几乎没有区分力。客户端可以调用它、把它传给别的函数、在分支里反复使用它，最后把差异转成布尔结果或发散。

定义不是要求枚举所有客户端。要否定等价，找一个区分上下文即可；要证明等价，则常用组合语义或逻辑关系一次覆盖全部构造。两种证明任务的量词负担不同。

例子与边界

两个对正常布尔输入相同的函数

令

k=\lambda x:\mathsf{Bool}.\mathsf{true},\qquad s=\lambda x:\mathsf{Bool}.\mathsf{if}\ x\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{true}.

两者类型均为 $\mathsf{Bool}\to\mathsf{Bool}$ ，对 true 和 false 都返回 true。但 $C=[\ ]\,\Omega$ 是合法的闭合 Bool 上下文，且

C[k]\to\mathsf{true},\qquad C[s]\to\mathsf{if}\ \Omega\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{true}\to\cdots.

因此观察分别为 $T$ 与 $\bot$ ，有 $k\not\simeq_{\mathrm{ctx}}s$ 。原因是 $s$ 必须读取守卫， $k$ 完全不读取参数；测试两个正常布尔输入没有覆盖这个差别。

上下文组合给出可替换性

关系的自反、对称、传递性直接来自观察相等。它还对良类型程序上下文封闭：若 $e\simeq_{\mathrm{ctx}}e'$ ，且 $D[e],D[e']$ 为同型闭项，则对任何闭合 Bool 测试 $C$ ，复合上下文 $C[D[\ ]]$ 仍是原定义允许的测试，所以两次观察相同。这证明 $D[e]\simeq_{\mathrm{ctx}}D[e']$ ，并解释为何定义要量化任意程序位置。

空上下文只适用于 Bool 洞；函数洞需要通过调用等操作变成布尔观察。对于本语言的闭合 Bool 项，同一观察确实足以推出上下文等价：由计算充分性取得观察与布尔指称的对应，再用组合性传播相等。高阶接口则还需考察客户端如何使用函数，前面的 $k,s$ 正展示了这种额外测试。

推论与应用

程序优化中的“替换部件”自然使用上下文等价，前提是优化承诺的观察与本文相同。例如恒等函数 $\lambda x.x$ 与 $\lambda x.(\lambda y.y)x$ 在这里等价；它们的指称相同，组合性与充分性给出所有上下文中的观察相同。若另把执行步数列为观察，这个证明目标就变了。

本单元的入口任务是给 $k,s,C$ 定型并算出 $T,\bot$ 。进阶任务见完全抽象：构造两个在所有 $L$ 上下文中等价、却被某个数学语义输入区分的高阶项。该反例解释“程序可观察的差异”与“模型容纳的差异”为何可能不一致。

参考资料

A. M. Pitts、G. Winskel、M. Fiore、M. Lennon-Bertrand，Denotational Semantics，2024-12-05 版，§5.3。该讲义使用更大的 PCF；本文明确限制到 Bool、箭头和原始发散常量的语言 $L$ 。

形式陈述 ​

先固定语言和观察 ​

量化全部程序上下文 ​

两个对正常布尔输入相同的函数 ​

上下文组合给出可替换性 ​

反向链接

形式陈述

先固定语言和观察

量化全部程序上下文

两个对正常布尔输入相同的函数

上下文组合给出可替换性