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 Levy-Longo tree equivalence and Bohm tree equivalence (up to η). We argue that enf bisimilarity is the call-by-value analogue of Levy-Longo tree equivalence. Enf bisimilarity (up to η) is the congruence on source terms induced by the call-by-value CPS transform and Bohm 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.