Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in lambda-calculi by decomposing their normal forms into bisimilar subterms. Besides, they allow for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of eta-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding bisimulation up to context are sound. We illustrate our technique with three calculi: the call-by-value lambda-calculus, the call-by-value lambda-calculus with the delimited-control operators shift and reset, and the call-by-value lambda-calculus with the abortive control operators call cc and abort. In the first two cases, there was previously no sound bisimulation up to context validating the eta-law, whereas no theory of normal-form bisimulations for the calculus of abortive control has been presented before. Our results have been fully formalized in the Coq proof assistant.
@cite_28 , Lassen defines several equivalences for the call-by-name @math -calculus, depending on the chosen semantics. He defines and for the semantics based on reduction to head normal form (where @math -expansion applies to any term @math , not only to a value as in the call-by-value @math -calculus), and based on reduction to weak head normal form. (It does not make sense to consider a , since it would be unsound, e.g., it would relate a non-terminating term @math with a normal form @math .) The paper also defines a bisimulation up to context for each bisimilarity.
@cite_28
1537995368
Abstract On the basis of an operational bisimulation account of Bohm tree equivalence, a novel operationally-based development of the Bohm tree theory is presented, including an elementary congruence proof for Bohm tree equivalence. The approach is also applied to other sensible and lazy tree theories. Finally, a syntactic proof principle, called bisimulation up to context, is derived from the congruence proofs. It is used to give a simple syntactic proof of the least fixed point property of fixed point combinators. The paper surveys notions of bisimulation and trees for sensible λ-theories based on reduction to head normal forms as well as for lazy λ-theories based on weak head normal forms.