逻辑关系基本定理

形式陈述 ​

先固定语言的求值语义，以及按类型定义的值关系 $\mathcal{V}[[A]]$ 和计算关系 $\mathcal{E}[[A]]$。对上下文 $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$，写

$${\gamma }_1\mathcal{G}[[\mathrm{\Gamma }]]{\gamma }_2$$

表示两个闭合替换逐变量相关：对每个 $x_i:A_i$，有 $({\gamma }_1(x_i),{\gamma }_2(x_i))\in \mathcal{V}[[A_i]]$。逻辑关系公理库逻辑关系Logical relation · Logical predicate · Reducibility relation按类型结构定义值与计算之间的关系，用于把局部类型规则提升为终止、等价或参数性结论。基本定理的二元形式是

$$\frac{\mathrm{\Gamma }⊢e:A{\gamma }_1\mathcal{G}[[\mathrm{\Gamma }]]{\gamma }_2}{(e[{\gamma }_1],e[{\gamma }_2])\in \mathcal{E}[[A]]}.$$

一元形式把二元关系换成可计算性谓词：若替换给每个变量指派属于其类型谓词的值，则闭合后的项属于 $\mathcal{E}[[A]]$。常说的“自相关”不是任意两个同类型项相关，而是同一个良类型项在两个相关实例化与相关环境下满足关系。

证明按类型推导公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。作归纳公理库数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。。三个核心分支说明环境条件为何不可省略：

1. 变量分支中，$e=x$，结论直接来自 ${\gamma }_1\mathcal{G}[[\mathrm{\Gamma }]]{\gamma }_2$ 对 $x$ 的分量。
2. 抽象分支中，推导末步来自 $\mathrm{\Gamma },x:A⊢e:B$。为证明两个 λ 值在 $A\to B$ 处相关，任取相关输入 $v_1,v_2$，把替换扩展为 ${\gamma }_1[x\mapsto v_1]$ 与 ${\gamma }_2[x\mapsto v_2]$，再对函数体使用归纳假设。
3. 应用分支中，归纳假设分别给出函数项在 $A\to B$ 处相关、参数项在 $A$ 处相关；箭头关系的定义于是推出两次应用在 $B$ 处相关。

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

直觉 ​

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

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

例子与边界 ​

对简单类型 λ 演算，令 $\mathcal{E}[[A]]$ 表示“求值到 $\mathcal{V}[[A]]$ 中的值”。闭项 $\varnothing ⊢e:A$ 使用空替换，基本定理立即给出 $e\in \mathcal{E}[[A]]$，所以 $e$ 终止。这把可归约性证明公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个有类型的简单 λ 项的所有 β-归约序列都有限并到达正规形。的主要负担集中到关系定义、替换闭包和三个核心推导分支上。

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

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

推论与应用 ​

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