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.
| Author: | Manfred Schmidt-Schauß, David Sabel, Elena Machkasova |
|---|---|
| URN: | urn:nbn:de:hebis:30-77888 |
| Series (Serial Number) | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (40) |
| Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
| Place of publication: | Frankfurt [am Main] |
| Document Type: | Working Paper |
| Language: | English |
| Date of Publication (online): | 22.06.2010 |
| Year of first Publication: | 2010 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| Tag: | Kontextuelle Gleichheit contextual equivalence ; lambda calculus ; letrec; semantics |
| SWD-Keyword: | Formale Semantik ; Lambda-Kalkül |
| HeBIS PPN: | 224533819 |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Licence (German): | Veröffentlichungsvertrag für Publikationen ohne Print on Demand |





