Simulation in the call-by-need lambda-calculus with letrec

Manfred Schmidt-Schauss, David Sabel, Elena Machkasova

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    10 Scopus citations

    Abstract

    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.

    Original languageEnglish (US)
    Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010
    Pages295-310
    Number of pages16
    StatePublished - Dec 1 2010
    Event21st International Conference on Rewriting Techniques and Applications, RTA 2010 - Edinburgh, United Kingdom
    Duration: Jul 11 2010Jul 13 2010

    Publication series

    NameLeibniz International Proceedings in Informatics, LIPIcs
    Volume6
    ISSN (Print)1868-8969

    Conference

    Conference21st International Conference on Rewriting Techniques and Applications, RTA 2010
    CountryUnited Kingdom
    CityEdinburgh
    Period7/11/107/13/10

    Keywords

    • Bisimulation
    • Call-by-need
    • Contextual equivalence
    • Lambda calculus
    • Letrec
    • Semantics

    Cite this