Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus

Abstract

Bohm tree equivalence up to possibly infinite eta expansion for the pure lambda-calculus can be characterized as a bisimulation equivalence. We call this co-inductive syntactic theory extensional head normal form bisimilarity and in this paper we extend it to the lambdaFP-calculus (the lambda-calculus with functional and surjective pairing) and to two untyped variants of Parigot's lambdamu-calculus. We relate the extensional head normal form bisimulation theories for the different calculi via Fujita's extensional CPS transform into the lambdaFP-calculus. We prove that extensional hnf bisimilarity is fully abstract for the pure lambda-calculus by a co-inductive reformulation of Barendregt's proof for Bohm tree equivalence up to possibly infinite eta expansion. The proof uses the so-called Bohm-out technique from Bohm's proof of the separation property for the lambda-calculus. Moreover, we extend the full abstraction result to extensional hnf bisimilarity for the lambdaFP-calculus. For the "standard" lambdamu-calculus, the separation property fails, as shown by David and Py, and for the same reason extensional hnf bisimilarity is not fully abstract. However, an "extended" variant of the lambdamu-calculus satisfies the separation property, as shown by Saurin, and we show that extensional hnf bisimilarity is fully abstract for this extended lambdamu-calculus