Call-by-value Solvability
Luca Paolini; Simona Ronchi Della Rocca
RAIRO - Theoretical Informatics and Applications (2010)
- Volume: 33, Issue: 6, page 507-534
- ISSN: 0988-3754
Access Full Article
top
Abstract
topHow to cite
topPaolini, Luca, and Simona Ronchi Della Rocca. "Call-by-value Solvability." RAIRO - Theoretical Informatics and Applications 33.6 (2010): 507-534. <http://eudml.org/doc/222050>.
@article{Paolini2010,
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.
},
author = {Paolini, Luca, Simona Ronchi Della Rocca},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Models of computations; λ-calculus; call-by-value.; solvability; -calculus},
language = {eng},
month = {3},
number = {6},
pages = {507-534},
publisher = {EDP Sciences},
title = {Call-by-value Solvability},
url = {http://eudml.org/doc/222050},
volume = {33},
year = {2010},
}
TY - JOUR
AU - Paolini, Luca
AU - Simona Ronchi Della Rocca
TI - Call-by-value Solvability
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 6
SP - 507
EP - 534
AB -
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.
LA - eng
KW - Models of computations; λ-calculus; call-by-value.; solvability; -calculus
UR - http://eudml.org/doc/222050
ER -
References
top- 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.
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.