2005 | OriginalPaper | Buchkapitel
Sharing in the Weak Lambda-Calculus
verfasst von : Tomasz Blanc, Jean-Jacques Lévy, Luc Maranget
Erschienen in: Processes, Terms and Cycles: Steps on the Road to Infinity
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Despite decades of research in the
λ
-calculus, the syntactic properties of the weak
λ
-calculus did not receive great attention. However, this theory is more relevant for the implementation of programming languages than the usual theory of the strong
λ
-calculus. In fact, the frameworks of weak explicit substitutions, or computational monads, or
λ
-calculus with a
let
statement, or super-combinators, were developed for adhoc purposes related to programming language implementation. In this paper, we concentrate on sharing of subterms in a confluent variant of the weak
λ
-calculus. We introduce a labeling of this calculus that expresses a confluent theory of reductions with sharing, independent of the reduction strategy. We finally state that Wadsworth’s evaluation technique with sharing of subterms corresponds to our formal setting.