LOGICAL STEP-INDEXED LOGICAL RELATIONS
LOGICAL STEP-INDEXED LOGICAL RELATIONS
复制标题
DOI：
10.2168/lmcs-7(2:16)2011
复制
发表时间：
2011-01-01
影响因子：
0.6
通讯作者：
Birkedal, Lars
中科院分区：
文献类型：
--
作者：
Dreyer, Derek;Ahmed, Amal;Birkedal, Lars
Appel 和 McAllester 的“步进索引”逻辑关系已被证明是一种简单而有效的技术，用于推理具有语义上有趣的类型（例如一般递归类型和一般引用类型）的语言中的程序。然而，使用阶跃索引模型的证明通常涉及繁琐、容易出错和证明模糊的阶跃索引算法，因此开发干净、高级、避免提及阶跃索引的等式证明原理非常重要。在本文中，我们展示了如何以抽象和优雅的方式推理二元阶跃索引逻辑关系。具体来说，我们定义了一个逻辑 LSLR，它受到 Plotkin 和 Abadi 参数化逻辑的启发，但也支持通过 Appel、Mellies、Richards 和 Vouillon 的“非常模态模型”论文中的模态“稍后”运算符来递归定义关系。我们在 LSLR 中编码一个逻辑关系，用于对用一般递归类型扩展的按值调用系统 F 中的程序进行关系推理。利用这种逻辑关系，我们推导出一组有用的规则，通过这些规则我们可以证明上下文等价性和近似结果，而无需计算步骤。
Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices.In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel, Mellies, Richards, and Vouillon's "very modal model" paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.