Equivalence of call-by-name and call-by-need for lambda-calculi with letrec
- We develop a proof method to show that in a (deterministic) lambda calculus with letrec and equipped with contextual equivalence the call-by-name and the call-by-need evaluation are equivalent, and also that the unrestricted copy-operation is correct. Given a let-binding x = t, the copy-operation replaces an occurrence of the variable x by the expression t, regardless of the form of t. This gives an answer to unresolved problems in several papers, it adds a strong method to the tool set for reasoning about contextual equivalence in higher-order calculi with letrec, and it enables a class of transformations that can be used as optimizations. The method can be used in different kind of lambda calculi with cyclic sharing. Probably it can also be used in non-deterministic lambda calculi if the variable x is "deterministic", i.e., has no interference with non-deterministic executions. The main technical idea is to use a restricted variant of the infinitary lambda-calculus, whose objects are the expressions that are unrolled w.r.t. let, to define the infinite developments as a reduction calculus on the infinite trees and showing a standardization theorem.
Verfasserangaben: | Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30-31771 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/schauss/cbneedname-inftree.pdf |
Titel des übergeordneten Werkes (Englisch): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 25 |
Schriftenreihe (Bandnummer): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (25) |
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 |
Datum der Veröffentlichung (online): | 29.09.2006 |
Datum der Erstveröffentlichung: | 29.09.2006 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 29.09.2006 |
Freies Schlagwort / Tag: | Kontextuelle Gleicheit; verzögerte Auswertung call-by-name; call-by-need; infinitary lambda calculus; lambda-calculus; lazy evaluation; letrec |
GND-Schlagwort: | Lambda-Kalkül; Programmtransformation |
Ausgabe / Heft: | Vers.: 29. September 2006 |
Seitenzahl: | 21 |
Letzte Seite: | 21 |
Quelle: | Technical Report Frank 25, Institut für Informatik, Johann Wolfgang Goethe-Universität Frankfurt am Main |
HeBIS-PPN: | 34437663X |
Institute: | Informatik und Mathematik / Informatik |
DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Lizenz (Deutsch): | Deutsches Urheberrecht |