Abstract
In Plotkin’s call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin’s original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable.
Chapter PDF
Similar content being viewed by others
Keywords
References
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984)
Barendregt, H.: Solvability in lambda-calculi. J. Symb. Logic 75(3), 191–231 (1975)
Wadsworth, C.: The Relation Between Computational and Denotational Properties for Scott’s D ∞ -Models of the λ-Calculus. SIAM J. Comput. 5(3), 488–521 (1976)
Plotkin, G.: Call-by-Name, Call-by-Value and the λ-Calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
Accattoli, B., Paolini, L.: Call-by-Value Solvability, Revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4–16. Springer, Heidelberg (2012)
Paolini, L., Ronchi Della Rocca, S.: Call-by-value Solvability. ITA 33(6), 507–534 (1999)
Paolini, L., Ronchi Della Rocca, S.: The Parametric λ-calculus: a Metamodel for Computation. Texts in Theoretical Computer Science. Springer, Berlin (2004)
Paolini, L., Pimentel, E., Ronchi Della Rocca, S.: Strong Normalization from an unusual point of view. Theor. Comput. Sci. 412(20), 1903–1915 (2011)
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(4), 461–482 (1995)
Moggi, E.: Computational Lambda-Calculus and Monads. In: LICS, pp. 14–23 (1989)
Dyckhoff, R., Lengrand, S.: Call-by-Value lambda-calculus and LJQ. J. Log. Comput. 17(6), 1109–1134 (2007)
Egidi, L., Honsell, F., Ronchi Della Rocca, S.: Operational, denotational and logical descriptions: a case study. Fundamenta Informaticæ 16(2), 149–169 (1992)
Ehrhard, T.: Collapsing non-idempotent intersection types. In: CSL, pp. 259–273 (2012)
Bucciarelli, A., Carraro, A., Ehrhard, T., Manzonetto, G.: Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion. Logical Methods in Computer Science 8(4) (2012)
Girard, J.: Linear Logic. Theor. Comput. Sci. 50(1), 1–102 (1987)
Regnier, L.: Lambda calcul et réseaux. PhD thesis, Université Paris 7 (1992)
Regnier, L.: Une équivalence sur les lambda-termes. Theor. Comput. Sci. 126(2), 281–292 (1994)
Melliès, P.: Categorical semantics of Linear Logic. In: Interactive Models of Computation and Program Behaviour. Panoramas et Synthèses, vol. 27, pp. 1–196. Société Mathématique de France (2009)
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)
Accattoli, B., Kesner, D.: The Permutative λ-Calculus. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol. 7180, pp. 23–36. Springer, Heidelberg (2012)
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
Carraro, A., Guerrieri, G. (2014). A Semantical and Operational Account of Call-by-Value Solvability. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)