Since 2014
Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution
|
|
| Creator |
Benaissa, Zine-El-Abidine
Lescanne, Pierre Rose, Kristoffer H. |
|
| Description |
We present the lambda sigma^a_w calculus, a formal synthesis of the concepts ofsharing and explicit substitution for weak reduction. We show howlambda sigma^a_w can be used as a foundation of implementations of functionalprogramming languages by modelling the essential ingredients of suchimplementations, namely weak reduction strategies, recursion, spaceleaks, recursive data structures, and parallel evaluation, in a uniform way.First, we give a precise account of the major reduction strategiesused in functional programming and the consequences of choosing lambda-graph-reduction vs. environment-based evaluation. Second, we showhow to add constructors and explicit recursion to give a precise accountof recursive functions and data structures even with respect tospace complexity. Third, we formalize the notion of space leaks in lambda sigma^a_wand use this to define a space leak free calculus; this suggests optimisationsfor call-by-need reduction that prevent space leaking and enablesus to prove that the "trimming" performed by the STG machine doesnot leak space.In summary we give a formal account of several implementationtechniques used by state of the art implementations of functional programminglanguages.Keywords. Implementation of functional programming, lambdacalculus, weak reduction, explicit substitution, sharing, recursion, spaceleaks.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1996-06-26
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18681
10.7146/brics.v3i56.18681 |
|
| Source |
BRICS Report Series; No 56 (1996): RS-56 Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution
BRICS Report Series; Nr. 56 (1996): RS-56 Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18681/16336
|
|