The notion of solvability in the call-by-value $lambda$-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 $eta$-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.

Call-by-Value Solvability

PAOLINI, LUCA LUIGI
First
;
RONCHI DELLA ROCCA, Simonetta
Last
1999-01-01

Abstract

The notion of solvability in the call-by-value $lambda$-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 $eta$-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.
33(6)
507
534
http://www.di.unito.it/~paolini/
https://doi.org/10.1051/ita:1999130
Models of computations; lambda-calculus; call-by-value.
L. PAOLINI; S. RONCHI DELLA ROCCA
File in questo prodotto:
File Dimensione Formato  
Call-by-Value Solvability - ITA 1999 ori.pdf

Accesso aperto

Tipo di file: PDF EDITORIALE
Dimensione 249.15 kB
Formato Adobe PDF
249.15 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/8397
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 34
  • ???jsp.display-item.citation.isi??? 19
social impact