Relational reasoning about contexts
Relational reasoning about contexts
复制标题
关于上下文的关系推理
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Søren B. Lassen
中科院分区：
文献类型：
--
作者：
Søren B. Lassen
操作推理的句法性质需要处理术语上下文的技术，尤其是关于递归的推理。在本文中，我们研究了小型按值调用函数语言的应用互模拟和 Sands 改进理论的变体。我们探索一种间接的、关系性的方法来推理上下文。它的灵感来自于 Howe 证明模拟顺序一致性的精确方法，以及 Pitts 证明适用于上下文的互模拟的扩展。我们通过展开定理和句法连续性的证明来说明这种方法，更重要的是，我们建立了 Sangiorgi 互模拟的类似物，以实现应用互模拟和改进。使用这些强大的上下文互模拟技术，我们给出了递归归纳、改进定理和句法最小不变性的简明操作证明。先前对这些结果的操作证明涉及对上下文的复杂、明确的推理。
The syntactic nature of operational reasoning requires techniques to deal with term contexts, especially for reasoning about recursion. In this paper we study applicative bisimulation and a variant of Sands’ improvement theory for a small call-by-value functional language. We explore an indirect, relational approach for reasoning about contexts. It is inspired by Howe’s precise method for proving congruence of simulation orderings and by Pitts’ extension thereof for proving applicative bisimulation up to context. We illustrate this approach with proofs of the unwinding theorem and syntactic continuity and, more importantly, we establish analogues of Sangiorgi’s bisimulation up to context for applicative bisimulation and for improvement. Using these powerful bisimulation up to context techniques, we give concise operational proofs of recursion induction, the improvement theorem, and syntactic minimal invariance. Previous operational proofs of these results involve complex, explicit reasoning about contexts.