Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-28T04:37:30.952Z Has data issue: false hasContentIssue false
  • English
  • Français

Call-by-value Solvability

Published online by Cambridge University Press:  15 August 2002

Luca Paolini  and
Simona Ronchi Della Rocca
Luca Paolini
Affiliation:
DISI, Università di Genova, Dipartimento di Informatica e Scienze dell'Informazione, Via Dodecaneso 35, 16146 Genova, Italy; [email protected].
Simona Ronchi Della Rocca
Affiliation:
Università di Torino, Dipartimento di Informatica, C.so Svizzera 185, 10149 Torino, Italy; [email protected].
Get access

Abstract

The notion of solvability in the call-by-value λ-calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical β-reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment system, assigning types of a given shape to all and only the call-by-value solvable terms.

Keywords

Models of computationsλ-calculuscall-by-value.
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 33 , Issue 6 , November 1999 , pp. 507 - 534
Copyright
© EDP Sciences, 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

S. Abramsky and C.H.L. Ong, Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105 (1993) 159-267.
H. Barendregt, The Lambda Calculus: Its syntax and semantics. North Holland (1984).
H. Barendregt, M. Coppo and M. Dezani-Ciancaglini, A filter Lambda Model and the completeness of type assignment. J. Symbolic Logic 48 (1983) 85-116.
L. Egidi, F. Honsell and S. Ronchi Della Rocca, Operational, denotational and logicals descriptions: A case study. Fund. Inform. (1992) 149-169.
J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ-Calculus. Cambridge University Press (1986).
F. Honsell and S. Ronchi Della Rocca, An Approximation Theorem for topological lambda models and the topological incompleteness of Lambda Calculus. J. Comput. Systems Sci. 45 (1992) 49-75.
M. Hyland, A syntactic characterization of the equalityin some Models for the Lambda Calculus. J. London Math. Soc. (1976) 361-370.
P.J. Landin, The mechanical evaluation of expressions. Comput. J. (1964).
R. Milner, M. Tofte and R. Harfen, The definition of standard ML, M.I.T. (1990).
L. Paolini, La chiamata per valore e la valutazione pigra nel lambda calcolo. Tesi di Laurea, Universitá di Torino, Dip. Informatica (1997).
G. Plotkin, Call by value, call by name and the λ-calculus. Theoret. Comput. Sci. (1975) 125-159.
S. Ronchi Della Rocca, Basic λ-calculus. Notes for the Summer School Proof and Types, Chambery (1993).
G.L. Steele and G.J. Sussman, The revised report on Scheme, AI Memo 452, M.I.T. (1978).
S. Thompson, HASKELL: The craft of functional programming. Addison-Wesley (1996).
C.P. Wadsworth, The relation between computational and denotational properties for Scott D∞-models of the lambda calculus. SIAM J. Comput. 5 (1976) 488-522.