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. Bisimilar
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.
show moreshow less

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-Schauß, David Sabel, Elena Machkasova
URN:urn:nbn:de:hebis:30-68385
DOI:http://dx.doi.org/10.4230/LIPIcs.RTA.2010.295
ISBN:978-3-939897-18-7
ISSN:1868-8969
Parent Title (English):Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA'10)
Publisher:Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH
Place of publication:Wadern
Document Type:Conference Proceeding
Language:English
Date of Publication (online):2010/12/01
Year of first Publication:2010
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Release Date:2010/12/01
Tag:bisimulation ; call-by-need; contextual equivalence ; lambda calculus ; letrec; semantics
Pagenumber:16
First Page:295
Last Page:310
Note:
(c) M. Schmidt-Schauß, D. Sabel, and E. Machkasova ; CC Creative Commons Non-Commercial No Derivatives License
Source:International Conference on Rewriting Techniques and Applications 2010 (Edinburgh), pp. 295-310 ; Digital Object Identifier: 10.4230/LIPIcs.RTA.2010.295
HeBIS PPN:229215289
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License LogoCreative Commons - Namensnennung-Nicht kommerziell-Keine Bearbeitung 3.0

$Rev: 11761 $