Linear-Time Self-Interpretation of the Pure Lambda Calculus |
| |
Authors: | Mogensen Torben Æ. |
| |
Affiliation: | (1) DIKU, University of Copenhagen, Denmark |
| |
Abstract: | We show that linear-time self-interpretation of the pure untyped lambda calculus is possible, in the sense that interpretation has a constant overhead compared to direct execution under various execution models. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use a self-interpreter based on previous work on self-interpretation and partial evaluation of the pure untyped lambda calculus.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term (using the same operational semantics).By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation (similar to graph reduction) and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably. |
| |
Keywords: | programs as data lambda calculus self-interpretation reduction order cost measures semantics |
本文献已被 SpringerLink 等数据库收录! |
|