Abstract
Call-by-value and call-by-need ł-calculi are defined using the distinguished syntactic category of values. In theoretical studies, values are variables and abstractions. In more practical works, values are usually defined simply as abstractions. This paper shows that practical values lead to a more efficient process of substitution—for both call-by-value and call-by-need—once the usual hypothesis for implementations hold (terms are closed, reduction does not go under abstraction, and substitution is done in micro steps, replacing one variable occurrence at the time). Namely, the number of substitution steps becomes linear in the number of β-redexes, while theoretical values only provide a quadratic bound.
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.
Similar content being viewed by others
References
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
Landin, P.J.: The Mechanical Evaluation of Expressions. The Computer Journal 6(4), 308–320 (1964)
Crank, E., Felleisen, M.: Parameter-passing and the lambda calculus. In: POPL, pp. 233–244 (1991)
Ronchi Della Rocca, S., Paolini, L.: The Parametric ł-Calculus. Springer, Heidelberg (2004)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Pfenning, F., Simmons, R.J.: Substructural operational semantics as ordered logic programming. In: LICS, pp. 101–110 (2009)
Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: RTA, pp. 6–21 (2012)
Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: RTA, pp. 22–37 (2012)
Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL, pp. 659–670 (2014)
Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP 2014 (accepted, 2014)
Accattoli, B., Dal Lago, U.: Beta Reduction is Invariant, Indeed. In: LICS/CSL 2014 (accepted, 2014)
Launchbury, J.: A natural semantics for lazy evaluation. In: POPL, pp. 144–154 (1993)
Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275–317 (1998)
Chang, S., Felleisen, M.: The call-by-need lambda calculus, revisited. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 128–147. Springer, Heidelberg (2012)
Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP, pp. 97–108 (2013)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Accattoli, B.: Proof nets and the call-by-value lambda-calculus. In: LSFA, pp. 11–26 (2012)
Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 163–174. Springer, Heidelberg (2009)
Wadsworth, C.P.: Some unusual λ-calculus numeral systems. In: Seldin, J., Hindley, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press (1980)
Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the lambda-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts (August 1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Accattoli, B., Sacerdoti Coen, C. (2014). On the Value of Variables. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2014. Lecture Notes in Computer Science, vol 8652. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44145-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-44145-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44144-2
Online ISBN: 978-3-662-44145-9
eBook Packages: Computer ScienceComputer Science (R0)