逻辑关系

形式陈述 ​

逻辑关系是一族由类型索引的关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。，其类型构造分支反映程序如何引入和使用该类型。以传值的简单类型 λ 演算为例，可先区分值解释 $\mathcal{V}[[A]]$ 与计算解释 $\mathcal{E}[[A]]$。用于证明终止的一元逻辑谓词可定义为

$$\begin{array}{rl}\mathcal{V}[[o]](v)& ⟺v\text{ 是指定的良类型基值},\\ \mathcal{V}[[A\to B]](v)& ⟺v\text{ 是函数值，且对每个 }{v}^{\prime }\in \mathcal{V}[[A]],\\ & v{v}^{\prime }\in \mathcal{E}[[B]],\\ \mathcal{E}[[A]](e)& ⟺\mathrm{\exists }v.e{\to }^{\ast }v\wedge \mathcal{V}[[A]](v).\end{array}$$

函数分支不是只检查函数自身是否终止，而是量化所有相关输入，因而沿类型结构携带可组合的行为条件。这里的 ${\to }^{\ast }$ 由所选运行语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。决定；换成传名、带错误或观察发散的语言，计算关系也必须相应改变。

二元逻辑关系把谓词改为两组程序间的关系。基类型先选定 $R_o$，箭头分支规定

$$(v_1,v_2)\in \mathcal{V}[[A\to B]]$$

当且仅当对所有 $(u_1,u_2)\in \mathcal{V}[[A]]$，应用 $v_1{u}_1$ 与 $v_2{u}_2$ 在 $\mathcal{E}[[B]]$ 下相关。一元形式常用于可计算性与正规化，二元形式常用于程序等价、表示独立和参数性；“逻辑关系”不是其中某一个具体定理的名称。

开放项还需要环境关系。若上下文公理库类型判断Typing judgment在上下文中断言项具有某类型的形式判断。 $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$，则两个闭合替换 ${\gamma }_1,{\gamma }_2$ 按 $\mathrm{\Gamma }$ 相关，意为每对 ${\gamma }_1(x_i),{\gamma }_2(x_i)$ 都落在 $\mathcal{V}[[A_i]]$。只有把开放项同时代入相关环境后，才能用闭项的运行关系讨论结果。

直觉 ​

普通类型说“这个值可被当作函数”，逻辑关系再问“它对所有合格输入都保持什么性质”。性质随类型递归传递：基值处给出观察标准，函数处要求把相关输入送到相关输出，积与和则逐字段或逐分支延伸。这样，局部类型规则不只是防止形状错误，还能把终止、等价或抽象不变量沿程序结构传下去。

“逻辑”主要指关系定义遵循类型或命题的结构，而不是说它等同于模型论中的逻辑关系或任意可写出的关系。真正可用于证明的关系还要与替换、求值和语言构造相容，并满足定义所需的闭包与良基条件。

例子与边界 ​

在一元终止谓词中，若 $v\in \mathcal{V}[[A\to B]]$ 且 $u\in \mathcal{V}[[A]]$，函数分支直接给出 $vu\in \mathcal{E}[[B]]$，因此应用会求值到一个相关的 $B$ 型值。证明良类型 λ 项都属于这族谓词时，变量分支必须从相关替换中取值；只定义闭项而忘记环境，就无法处理函数体中的自由变量。

二元例子可把两个整数栈实现联系起来：只要基于数组的值与基于列表的值表示同一抽象序列，push、pop 对相关输入保持这一关系，客户端便可在接口结果上得到相同观察。这里需要的是操作保持的关系，不是“两个实现类型相同”这一事实本身。

递归类型会让“按类型直接递归”再次遇到同一个类型，定义不再显然良基；可变状态又使相关性依赖未来可访问的堆。step-indexed 关系用剩余观察步数打断递归，Kripke 关系用 possible worlds 记录堆不变量及其扩展。它们不是基础关系的装饰，而是对应语言特性所需的良基和状态结构。

推论与应用 ​

逻辑关系是证明类型化正规化公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个有类型的简单 λ 项的所有 β-归约序列都有限并到达正规形。、上下文等价、编译保持与参数多态公理库参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。约束的通用方法框架。实际结论来自一个另外证明的基本引理：良类型项在相关环境下产生相关结果；本页给出关系对象与开放项接口，不把该引理当作定义的一部分。

选择关系时必须先固定语言、类型解释和可观察行为。若异常是否相同、发散是否可区分、分配地址是否可见尚未说明，就不能声称关系蕴含程序等价。关系越精确，证明负担通常越高；关系过弱则可能无法推出目标观察结论。

参考资料

• William W. Tait, “Intensional Interpretations of Functionals of Finite Type I,” Journal of Symbolic Logic 32(2), 1967，computability method。
• Andrew M. Pitts, Operational Semantics and Program Equivalence, in Applied Semantics, Springer, 2002，logical relations and operational equivalence。
• Amal Ahmed, “Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types,” ESOP, 2006。