TY  - UNPD
A1  - Schmidt-Schauß, Manfred
T1  - Equivalence of call-by-name and call-by-need for lambda-calculi with letrec
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 25
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 25 [v.2] 
KW  - Lambda-Kalkül
KW  - Programmtransformation
KW  - call-by-name
KW  - call-by-need
KW  - infinitary lambda calculus
KW  - lambda-calculus
KW  - lazy evaluation
KW  - letrec
Y1  - 2007
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34424
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344247
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/schauss/cbneedname-inftree-V2.pdf
IS  - Version: 29 Januar 2007
EP  - 24
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -