Name
Abstract | ||
|---|---|---|
We present a name free λ-calculus with explicit substitutions based on a generalized notion of director strings: we annotate a term with information about how each substitution should be propagated through the term. We first present a calculus where we can simulate arbitrary β-reduction steps, and then simplify the rules to model the evaluation of functional programs (reduction to weak head normal form). We also show that we can derive the closed reduction strategy (a weak strategy which, in contrast with standard weak strategies allows certain reductions to take place inside λ-abstractions thus offering more sharing). Our experimental results confirm that, for large combinator based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/3-540-44881-0_5 | RTA |
Keywords | Field | DocType |
efficient reduction,weak strategy,closed reduction strategy,weak evaluation strategy,standard weak strategy,standard evaluator,certain reduction,strong reduction,director string,weak evaluator,reduction step,weak head,abstract machine,normal form,functional programming | Reduction strategy,Computer science,Combinatory logic,Algorithm,Weak solution,Rewriting,Director string,String (computer science),Abstract machine,Calculus,Proof assistant | Conference |
Volume | ISSN | ISBN |
2706 | 0302-9743 | 3-540-40254-3 |
Citations | PageRank | References |
9 | 0.56 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| François-régis Sinot | 1 | 74 | 6.84 |
| Maribel Fernández | 2 | 315 | 23.44 |
| Ian Mackie | 3 | 88 | 9.58 |