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

Abstract

top
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.

How to cite

top

Paolini, 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
  1. S. Abramsky and C.H.L. Ong, Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105 (1993) 159-267.  Zbl0779.03003
  2. H. Barendregt, The Lambda Calculus: Its syntax and semantics. North Holland (1984).  Zbl0551.03007
  3. 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.  Zbl0545.03004
  4. L. Egidi, F. Honsell and S. Ronchi Della Rocca, Operational, denotational and logicals descriptions: A case study. Fund. Inform. (1992) 149-169.  
  5. J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ-Calculus. Cambridge University Press (1986).  Zbl0614.03014
  6. 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.  Zbl0763.03012
  7. M. Hyland, A syntactic characterization of the equalityin some Models for the Lambda Calculus. J. London Math. Soc. (1976) 361-370.  Zbl0329.02010
  8. P.J. Landin, The mechanical evaluation of expressions. Comput. J. (1964).  Zbl0122.36106
  9. R. Milner, M. Tofte and R. Harfen, The definition of standard ML, M.I.T. (1990).  
  10. L. Paolini, La chiamata per valore e la valutazione pigra nel lambda calcolo. Tesi di Laurea, Universitá di Torino, Dip. Informatica (1997).  
  11. G. Plotkin, Call by value, call by name and the λ-calculus. Theoret. Comput. Sci. (1975) 125-159.  Zbl0325.68006
  12. S. Ronchi Della Rocca, Basic λ-calculus. Notes for the Summer School Proof and Types, Chambery (1993).  
  13. G.L. Steele and G.J. Sussman, The revised report on Scheme, AI Memo 452, M.I.T. (1978).  
  14. S. Thompson, HASKELL: The craft of functional programming. Addison-Wesley (1996).  
  15. 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.  Zbl0346.02013

NotesEmbed ?

top

You 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.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.