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.
Verfasserangaben: | Manfred Schmidt-SchaußORCiDGND, David SabelORCiDGND, Elena Machkasova |
---|---|
URN: | urn:nbn:de:hebis:30-77888 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-40.pdf |
Titel des übergeordneten Werkes (Deutsch): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 40 |
Schriftenreihe (Bandnummer): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (40) |
Verlag: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
Verlagsort: | Frankfurt [am Main] |
Dokumentart: | Arbeitspapier |
Sprache: | Englisch |
Jahr der Fertigstellung: | 2010 |
Jahr der Erstveröffentlichung: | 2010 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 22.06.2010 |
Freies Schlagwort / Tag: | Kontextuelle Gleichheit contextual equivalence; lambda calculus; letrec; semantics |
GND-Schlagwort: | Formale Semantik; Lambda-Kalkül |
Seitenzahl: | 34 |
HeBIS-PPN: | 224533819 |
Institute: | Informatik und Mathematik / Informatik |
DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Lizenz (Deutsch): | Deutsches Urheberrecht |