Eager normal form bisimulation
Eager normal form bisimulation
复制标题
渴望正常形式互模拟
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Søren B. Lassen
中科院分区：
文献类型：
--
作者：
Søren B. Lassen
本文描述了纯无类型按值调用/SPL lambda/-演算的两个新的互模拟等价，称为enf互相似和enf互相似，直到/SPL ETA/。它们基于项到急切范式(ENF)的急切约简，类似于Levy-Longo树等价和Bohm树等价(Up/SPL ETA/)的共归纳互模拟特征。我们认为enf bisimily是Levy-Longo树等价的按值调用的类比。ENF双向相似性(高达/SPL ETA/)是由按值调用CPS变换和目标项上的Bohm树等价(高达/SPL ETA/)在源项上产生的同余。EnF互相似和enf互相似高达/SPL ETA/享受强大的互模拟证明原理，其中，这些原理可用于建立按值调用CPS变换的收缩定理。
This paper describes two new bisimulation equivalences for the pure untyped call-by-value /spl lambda/-calculus, called enf bisimilarity and enf bisimilarity up to /spl eta/. They are based on eager reduction of terms to eager normal form (enf), analogously to co-inductive bisimulation characterizations of Levy-Longo tree equivalence and Bohm tree equivalence (up to /spl eta/). We argue that enf bisimilarity is the call-by-value analogue of Levy-Longo tree equivalence. Enf bisimilarity (up to /spl eta/) is the congruence on source terms induced by the call-by-value CPS transform and Bohm tree equivalence (up to /spl eta/) on target terms. Enf bisimilarity and enf bisimilarity up to /spl eta/ enjoy powerful bisimulation proof principles which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.