Head Normal Form Bisimulation for Pairs and the λμ-Calculus (Extended Abstract)
Søren B. Lassen · 2006
Böhm tree equivalence up to possibly infinite η expan-sion for the pure λ-calculus can be characterized as a bisimulation equivalence. We call this co-inductive syntac-tic theory extensional head normal form bisimilarity and in this paper we extend it to the λFP-calculus (the λ-calculus with functional and surjective pairing) and to two untyped variants of Parigot’s λμ-calculus. We relate the extensional head normal form bisimulation theories for the different calculi via Fujita’s extensional CPS transform into the λFP-calculus. We prove that extensional hnf bisimilarity is fully abstract for the pure λ-calculus by a co-inductive refor-mulation of Barendregt’s proof for Böhm tree equivalence up to possibly infinite η expansion. The proof uses the so-called Böhm-out technique from Böhm’s proof of the Sep-aration Property for the λ-calculus. Moreover, we extend the full abstraction result to extensional hnf bisimilarity for the λFP-calculus. For the “standard ” λμ-calculus, the Sep-aration Property fails, as shown by David and Py, and for the same reason extensional hnf bisimilarity is not fully ab-stract. However, an “extended ” variant of the λμ-calculus satisfies the Separation Property, as shown by Saurin, and for this extended λμ-calculus. 1