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
Author:Manfred Schmidt-SchaußORCiDGND
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 [v.2])
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
Place of publication:Frankfurt am Main
Document Type:Working Paper
Date of Publication (online):2007/01/29
Date of first Publication:2007/01/29
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2014/07/08
Tag:call-by-name; call-by-need; infinitary lambda calculus; lambda-calculus; lazy evaluation; letrec
GND Keyword:Lambda-Kalkül; Programmtransformation
Issue:Version: 29 Januar 2007
Page Number:24
Last Page:24
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