This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.
@InProceedings{schmidtschauss_et_al:LIPIcs.RTA.2010.295, author = {Schmidt-Schauss, Manfred and Sabel, David and Machkasova, Elena}, title = {{Simulation in the Call-by-Need Lambda-Calculus with letrec}}, booktitle = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications}, pages = {295--310}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-18-7}, ISSN = {1868-8969}, year = {2010}, volume = {6}, editor = {Lynch, Christopher}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.295}, URN = {urn:nbn:de:0030-drops-26593}, doi = {10.4230/LIPIcs.RTA.2010.295}, annote = {Keywords: Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need} }
Feedback for Dagstuhl Publishing