Eager Normal Form Bisimulation

This paper describes two new bisimulation equivalences for the pure untyped call-by-value λ-calculus, called enf bisimilarity and enf bisimilarity up to η. They are based on eager reduction of terms to eager normal form (enf), analogously to co-inductive bisimulation characterizations of L´evy-Longo tree equivalence and B¨ohm tree equivalence (up to η). We argue that enf bisimilarity is the call-by-value analogue of L´evy-Longo tree equivalence. Enf bisimilarity (up to η) is the congruence on source terms induced by the call-by-value CPS transform and B¨ohm tree equivalence (up to η) on target terms. Enf bisimilarity and enf bisimilarity up to η enjoy powerful bisimulation proof principles which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.

• Type: Conference
• Year: 2005
• Where: LICS
• Authors: Soren Lassen
• Keywords: Computer Science, Enf Bisimilarity, LICS 2005, L´evy-Longo Tree Equivalence, Tree Equivalence