Schmidt-Schauss, Manfred ;
Sabel, David ;
Machkasova, Elena
Simulation in the Call-by-Need Lambda-Calculus with letrec
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.
BibTeX - Entry
@InProceedings{schmidtschauss_et_al:LIPIcs:2010:2659,
author = {Manfred Schmidt-Schauss and David Sabel and Elena Machkasova},
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 = {Christopher Lynch},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2659},
URN = {urn:nbn:de:0030-drops-26593},
doi = {http://dx.doi.org/10.4230/LIPIcs.RTA.2010.295},
annote = {Keywords: Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need}
}
|
Keywords: |
|
Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need |
|
Seminar: |
|
Proceedings of the 21st International Conference on Rewriting Techniques and Applications
|
|
Issue date: |
|
2010 |
|
Date of publication: |
|
2010 |
