Abstract
We show that linear time self-interpretation of the pure untyped lambda calculus is possible. 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 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.
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 and cost of an environment-based implementation.
For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
I. Durand and A. Middeldorp. Decidable call by need computations in term rewriting. In CADE’ 97, Lecture Notes in Artificial Intelligence 1249, pages 4–18. Springer-Verlag, 1997.
N. D. Jones. Constant time factors do matter. In Steven Homer, editor, STOC’ 93. Symposium on Theory of Computing, pages 602–611. ACM Press, 1993.
J. L. Lawall and H. G. Mairson. Optimality and ineffciency: What isn’t a cost model of the lambda calculus. In R. Kent Dybvig, editor, Proceedings of ICFP’ 95, pages 92–101. ACM, ACM Press, 1996.
T. Æ. Mogensen. Efficient self-interpretation in lambda calculus. Functional Programming, 2(3):345–364, July 1992.
T. Æ. Mogensen. Self-applicable online partial evaluation of the pure lambda calculus. In William L. Scherlis, editor, Proceedings of PEPM’ 95, pages 39–44. ACM, ACM Press, 1995.
Eva Rose. Characterizing computation models with a constant factor time hierachy. In B. Kapron, editor, DIMACS Workshop On Computational Complexity and Programming Languages, New Jersey, USA, July 1996. DIMACS, RUTCOR, Rutgers University.
Eva Rose. Linear time hierachies for a functional language machine model. In Hanne Riis Nielson, editor, Programming Languages and Systems — ESOP’96, volume 1058 of LNCS, pages 311–325, Linköping, Sweden, Apr 1996. Linköping University, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mogensen, T.Æ. (2000). Linear Time Self-Interpretation of the Pure Lambda Calculus. In: Bjøner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-46562-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67102-2
Online ISBN: 978-3-540-46562-1
eBook Packages: Springer Book Archive