Eager Normal Form Bisimulation

Abstract

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.