Simulation in the call-by-need lambda-calculus with letrec
- 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. 1998 ACM Subject Classification: F.4.2, F.3.2, F.3.3, F.4.1. Key words and phrases: semantics, contextual equivalence, bisimulation, lambda calculus, call-by-need, letrec.
Verfasserangaben: | Manfred Schmidt-SchaußORCiDGND, David SabelORCiDGND, Elena Machkasova |
---|---|
URN: | urn:nbn:de:hebis:30-68385 |
DOI: | https://doi.org/10.4230/LIPIcs.RTA.2010.295 |
ISBN: | 978-3-939897-18-7 |
ISSN: | 1868-8969 |
Titel des übergeordneten Werkes (Englisch): | Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA'10) |
Verlag: | Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH |
Verlagsort: | Wadern |
Dokumentart: | Konferenzveröffentlichung |
Sprache: | Englisch |
Datum der Veröffentlichung (online): | 01.12.2010 |
Jahr der Erstveröffentlichung: | 2010 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 01.12.2010 |
Freies Schlagwort / Tag: | bisimulation; call-by-need; contextual equivalence; lambda calculus; letrec; semantics |
Seitenzahl: | 16 |
Erste Seite: | 295 |
Letzte Seite: | 310 |
Bemerkung: | (c) M. Schmidt-Schauß, D. Sabel, and E. Machkasova ; CC Creative Commons Non-Commercial No Derivatives License |
Quelle: | International Conference on Rewriting Techniques and Applications 2010 (Edinburgh), pp. 295-310 ; Digital Object Identifier: 10.4230/LIPIcs.RTA.2010.295 |
HeBIS-PPN: | 229215289 |
Institute: | Informatik und Mathematik / Informatik |
DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Lizenz (Deutsch): | Creative Commons - Namensnennung-Nicht kommerziell-Keine Bearbeitung 3.0 |