Abstract
In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman’s call-by-value λ CBV calculus and from Accattoli and Kesner’s substitution calculus λ sub . In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.
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
Accattoli, B.: An abstract factorisation theorem for explicit substitutions (2011) (accepted at RTA 2012), https://sites.google.com/site/beniaminoaccattoli/factorisation.pdf
Accattoli, B.: Jumping around the box. Ph.D. Thesis, Università di Roma La Sapienza (2011)
Accattoli, B., Guerrini, S.: Jumping Boxes. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 55–70. Springer, Heidelberg (2009)
Accattoli, B., Kesner, D.: The Permutative λ-Calculus. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 23–36. Springer, Heidelberg (2012)
Accattoli, B., Kesner, D.: The Structural λ-Calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010)
Accattoli, B., Paolini, L.: Call-by-value solvability, revisited (ext. version) (2012), https://sites.google.com/site/beniaminoaccattoli/CBV-solvabilitywithproofs.pdf
Barendregt, H.P.: The Lambda Calculus – Its Syntax and Semantics, vol. 103. North-Holland (1984)
Barendregt, H.: Solvability in lambda-calculi. The Journal of Symbolic Logic 39(2), 372 (1975)
Dyckhoff, R., Lengrand, S.: Call-by-value lambda-calculus and ljq. J. Log. Comput. 17(6), 1109–1134 (2007)
Fernández, M., Siafakas, N.: Labelled lambda-calculi with explicit copy and erase. In: LINEARITY, pp. 49–64 (2009)
Herbelin, H., Zimmermann, S.: An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 142–156. Springer, Heidelberg (2009)
Hofmann, M.: Sound and complete axiomatisations of call-by-value control operators. Mathematical Structures in Computer Science 5, 461–482 (1995)
Hyland, J.M.E.: A Survey of Some Useful Partial Order Relations on Terms of the Lambda Calculus. In: Böhm, C. (ed.) λ-Calculus and Computer Science Theory. LNCS, vol. 37, pp. 83–95. Springer, Heidelberg (1975)
Klop, J.W.: On Solvability by λ I - Terms. In: Böhm, C. (ed.) λ-Calculus and Computer Science Theory. LNCS, vol. 37, pp. 342–345. Springer, Heidelberg (1975)
Landin, P.J.: A correspondence between ALGOL 60 and Church’s lambda-notation: Part I and Part II. Communications of the ACM 8(2-3), 89–101, 158–165 (1965)
Melliès, P.A.: A Factorisation Theorem in Rewriting Theory. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 49–68. Springer, Heidelberg (1997)
Moggi, E.: Computational lambda-calculus and monads. In: LICS, pp. 14–23. IEEE Computer Society Press, Piscataway (1989)
Pagani, M., Rocca, S.R.D.: Linearity, non-determinism and solvability. Fundam. Inform. 103(1-4), 173–202 (2010)
Paolini, L.: Call-by-Value Separability and Computability. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) ICTCS 2001. LNCS, vol. 2202, pp. 74–89. Springer, Heidelberg (2001)
Paolini, L., Pimentel, E., Ronchi Della Rocca, S.: Lazy strong normalization. Electr. Notes Theor. Comput. Sci. 136, 103–116 (2005)
Paolini, L., Ronchi Della Rocca, S.: Call-by-value solvability. Theoretical Informatics and Applications 33(6), 507–534 (1999)
Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)
Ronchi Della Rocca, S., Paolini, L.: The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS. Springer, Berlin (2004)
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP and Symbolic Computation 6, 289–360 (1993)
Saurin, A.: Standardization and Böhm Trees for Λμ-Calculus. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 134–149. Springer, Heidelberg (2010)
Wadsworth, C.P.: The relation between computational and denotational properties for Scott’s D ∞ -models of the lambda-calculus. SIAM Journal of Computing 5(3), 488–521 (1976)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Accattoli, B., Paolini, L. (2012). Call-by-Value Solvability, Revisited. In: Schrijvers, T., Thiemann, P. (eds) Functional and Logic Programming. FLOPS 2012. Lecture Notes in Computer Science, vol 7294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29822-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-29822-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29821-9
Online ISBN: 978-3-642-29822-6
eBook Packages: Computer ScienceComputer Science (R0)