Abstract
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by-value beta-reduction can be simulated by an orthogonal constructor term rewrite system in the same number of reduction steps. Conversely, each reduction in an orthogonal term rewrite system can be simulated by a constant number of weak call-by-value beta-reduction steps. This is relevant to implicit computational complexity, because the number of beta steps to normal form is polynomially related to the actual cost (that is, as performed on a Turing machine) of normalization, under weak call-by-value reduction. Orthogonal constructor term rewrite systems and lambda-calculus are thus both polynomially related to Turing machines, taking as notion of cost their natural parameters.
The authors are partially supported by PRIN project “CONCERTO” and FIRB grant RBIN04M8S8, “Intern. Inst. for Applicable Math.”
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H., Eekelen, M., Glauert, J., Kennaway, J., Plasmeijer, M., Sleep, M.: Term graph rewriting. In: de Bakker, J., Nijman, A., Treleaven, P. (eds.) Parallel Languages on PARLE: Parallel Architectures and Languages Europe, vol. II, pp. 141–158. Springer, Heidelberg (1986)
Barendsen, E.: Term graph rewriting. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems, pp. 712–743. Cambridge Univ. Press, Cambridge (2003)
Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity 2, 97–110 (1992)
Dal Lago, U., Martini, S.: An invariant cost model for the lambda-calculus. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 105–114. Springer, Heidelberg (2006)
Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. Extended Version (2009), http://arxiv.org/abs/0904.4120
Girard, J.-Y.: Light linear logic. Inform. and Comp. 143(2), 175–204 (1998)
Gurevich, Y.: The sequential ASM thesis. In: Current trends in theoretical computer science, pp. 363–392. World Scientific, Singapore (2001)
Jones, S.P.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)
Leivant, D.: Ramified recurrence and computational complexity I: word recurrence and poly-time. In: Feasible Mathematics II, pp. 320–343. Birkhäuser, Basel (1995)
Marion, J.-Y., Moyen, J.-Y.: Efficient first order functional program interpreter with time bound certifications. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol. 1955, pp. 25–42. Springer, Heidelberg (2000)
Parigot, M.: On the representation of data in lambda-calculus. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 309–321. Springer, Heidelberg (1990)
Parigot, M., Rozière, P.: Constant time reductions in lambda-caculus. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 608–617. Springer, Heidelberg (1993)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1(2), 125–159 (1975)
Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 60–82. Springer, Heidelberg (2002)
Splawski, Z., Urzyczyn, P.: Type fixpoints: Iteration vs. recursion. In: 4th International Conference on Functional Programming, Proceedings, pp. 102–113. ACM Press, New York (1999)
van Emde Boas, P.: Machine models and simulation. In: Handbook of Theoretical Computer Science, Algorithms and Complexity, pp. 1–66. MIT Press, Cambridge (1990)
Wadsworth, C.: Some unusual λ-calculus numeral systems. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Martini, S. (2009). On Constructor Rewrite Systems and the Lambda-Calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds) Automata, Languages and Programming. ICALP 2009. Lecture Notes in Computer Science, vol 5556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02930-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-02930-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02929-5
Online ISBN: 978-3-642-02930-1
eBook Packages: Computer ScienceComputer Science (R0)