A bisimulation for type abstraction and recursion
A bisimulation for type abstraction and recursion
复制标题
DOI：
10.1145/1040305.1040311
复制
发表时间：
2005-01
期刊：
影响因子：
--
通讯作者：
Eijiro Sumii;B. Pierce
中科院分区：
文献类型：
--
作者：
Eijiro Sumii;B. Pierce
我们提出了一种基于互模拟的可靠的、完整的和初等的证明方法，用于证明λ演算中的上下文等价性，包括全泛类型、存在类型和递归类型。与逻辑关系(语义或语法)不同，我们的开发是基本的，只使用集合和关系，并避免使用域理论、可容许性和ΤΤ闭包等高级机制。与其他互模拟不同，我们的互模拟即使对于存在主义类型也是完整的。关键的想法是将关系集-而不仅仅是关系-视为互模拟。
We present a sound, complete, and elementary proof method, based on bisimulation, for contextual equivalence in a λ-calculus with full universal, existential, and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary, using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and ΤΤ-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider sets of relations---instead of just relations---as bisimulations.