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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-SchaußORCiDGND
URN:urn:nbn:de:hebis:30-31771
URL:http://www.ki.informatik.uni-frankfurt.de/papers/schauss/cbneedname-inftree.pdf
Parent Title (English):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 25
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (25)
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):2006/09/29
Date of first Publication:2006/09/29
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2006/09/29
Tag:Kontextuelle Gleicheit; verzögerte Auswertung
call-by-name; call-by-need; infinitary lambda calculus; lambda-calculus; lazy evaluation; letrec
GND Keyword:Lambda-Kalkül; Programmtransformation
Issue:Vers.: 29. September 2006
Page Number:21
Last Page:21
Source:Technical Report Frank 25, Institut für Informatik, Johann Wolfgang Goethe-Universität Frankfurt am Main
HeBIS-PPN:34437663X
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht