逻辑关系基本定理 | Codeboy's Blog

形式陈述

本页陈述的是需要针对语言与关系共同证明的一类基本引理；任意挑一族按类型索引的关系，并不会自动得到结论。先固定语言的求值语义，以及按类型定义的值关系 $\mathcal V\llbracket A\rrbracket$ 和计算关系 $\mathcal E\llbracket A\rrbracket$ 。对上下文 $\Gamma=x_1:A_1,\ldots,x_n:A_n$ ，写

\gamma_1\mathrel{\mathcal G\llbracket\Gamma\rrbracket}\gamma_2

表示两个闭合替换逐变量相关：对每个 $x_i:A_i$ ，有 $(\gamma_1(x_i),\gamma_2(x_i))\in\mathcal V\llbracket A_i\rrbracket$ 。对每种原始常量和类型规则，都必须证明所选关系的相容性分支；例如布尔关系若连 true 与自身都不相关，含 true 的语言就不满足自相关结论。这些义务完成后，逻辑关系基本定理的二元形式是

\frac{ \Gamma\vdash e:A \qquad \gamma_1\mathrel{\mathcal G\llbracket\Gamma\rrbracket}\gamma_2 }{ (e[\gamma_1],e[\gamma_2]) \in\mathcal E\llbracket A\rrbracket }.

一元形式把二元关系换成可计算性谓词：若替换给每个变量指派属于其类型谓词的值，则闭合后的项属于 $\mathcal E\llbracket A\rrbracket$ 。这里展示的是传值、闭值环境的版本。完整 β 强正规化另用定义在可能开放的良类型项上的一元可归约谓词，替换也可取相关开项，而不限定为已求值的闭值；相应基本引理须在该谓词下重新证明。常说的“自相关”不是任意两个同类型项相关，而是同一个良类型项在两个相关实例化与相关环境下满足关系。

证明按类型推导作归纳。三个核心分支说明环境条件为何不可省略：

变量分支中， $e=x$ ，结论直接来自 $\gamma_1\mathrel{\mathcal G\llbracket\Gamma\rrbracket}\gamma_2$ 对 $x$ 的分量。
抽象分支中，推导末步来自 $\Gamma,x:A\vdash e:B$ 。为证明两个 λ 值在 $A\to B$ 处相关，任取相关输入 $v_1,v_2$ ，把替换扩展为 $\gamma_1[x\mapsto v_1]$ 与 $\gamma_2[x\mapsto v_2]$ ，再对函数体使用归纳假设。
应用分支中，归纳假设分别给出函数项在 $A\to B$ 处相关、参数项在 $A$ 处相关。对这里的传值终止关系，先取得两侧相关的函数值与参数值，再用箭头分支及计算关系的求值闭包，推出两次应用在 $B$ 处相关。

若语言含子类型、类型抽象、状态或递归，每种额外 typing rule 都会新增证明分支，并可能迫使关系加入闭包、world 或 step index。按裸项语法归纳会丢掉“最后使用了哪条类型规则”的信息，不能替代对推导树的归纳。

直觉

逻辑关系按类型规定局部行为，基本定理则证明整个类型系统不会越出这些规定。相关环境像一组接口契约：变量已经满足契约，抽象把契约延伸到任意相关实参，应用再把函数契约与参数契约扣合。证明逐条跟随 typing rule，因此每一种合法程序构造都被审计一次。

基本定理更像一个可复用的证明引擎，而不是一个固定结论。把基关系选成终止谓词，它导出正规化；选成两个实现的表示关系，它约束客户端观察；在 System F 中让类型变量解释为任意关系，则得到参数性。

例子与边界

对简单类型 λ 演算，令 $\mathcal E\llbracket A\rrbracket$ 表示“求值到 $\mathcal V\llbracket A\rrbracket$ 中的值”。闭项 $\varnothing\vdash e:A$ 使用空替换，基本定理立即给出 $e\in\mathcal E\llbracket A\rrbracket$ ，所以 $e$ 终止。这把可归约性证明的主要负担集中到关系定义、替换闭包和三个核心推导分支上。

若两个集合模块的内部值由“表示同一数学集合”关系连接，且每个导出操作保持该关系，基本定理可限制良类型客户端只能得到相关观察。不过它不会自动制造所需表示关系，也不会替代逐个验证模块操作保持关系的义务。

边界是把结论误读为“任意两个同类型程序都等价”。常量 true 与 false 同属布尔类型，却不会在取等关系的布尔解释下相关。关系还依赖语言观察：加入异常、非终止或可变状态后，沿用纯、总语言的 $\mathcal E$ 会遗漏真实行为，基本定理的陈述和证明都必须随之调整。

推论与应用

在带原始布尔发散常量的弱传名语言中，形式近似的基本引理逐项证明变量、常量、抽象、应用和条件式的归纳分支；条件式守卫为底而结果为函数时，要用“各类型底元近似任意项”的辅助引理。完全抽象反例还展示三元关系保持性与二元上下文相容性：前者排除一种不可定义输入，后者把应用测试结论提升到所有闭合布尔上下文。

同一充分性页的独立 $L_{\mathrm{fix}}$ 扩充还补齐不动点分支：逐个语义近似使用箭头关系，再在有限域的稳定位置收尾。计数器表示独立性则在纯传值语言中逐项证明二元环境引理，包括返回抽象状态的原始递归；两种证明的求值方式、计算关系及允许构造均明确分开。

逻辑关系基本定理把类型安全、正规化、编译器关系证明和抽象定理组织成同一种“良类型项保持关系”的结构。真正推出上下文等价时，还需证明逻辑关系对程序上下文充分、并与目标观察相容；基本定理本身只提供从 typing derivation 到关系成员的方向。

在机械化证明中，替换、环境扩展、弱化和类型替换常占据大量辅助引理。它们不是算法执行步骤，而是保证归纳假设可在新绑定下使用的元理论基础；省略这些条件会让纸面证明在 λ 抽象或多态分支处断裂。

参考资料

William W. Tait, “Intensional Interpretations of Functionals of Finite Type I,” Journal of Symbolic Logic 32(2), 1967。
Jean-Yves Girard, Proofs and Types, Cambridge University Press, 1989，reducibility candidates and fundamental lemmas。
Andrew M. Pitts, Operational Semantics and Program Equivalence, in Applied Semantics, Springer, 2002，logical relations and fundamental properties。

形式陈述 ​

反向链接

形式陈述