The aim of this paper is to study the notion of separability in the call-by-value setting. Separability is the key notion used in the Böhm Theorem, proving that syntactically different βη-normal forms are separable in the classical λ-calculus endowed with β-reduction, i.e. in the call-by-name setting. In the case of call-by-value λ-calculus endowed with β v-reduction and η v-reduction (see Plotkin [7]), it turns out that two syntactically different βη v-normal forms are separable too, while the notion of β v-normal form and βη v-normal form is semantically meaningless. An explicit representation of Kleene’s recursive functions is presented. The separability result guarantees that the representation makes sense in every consistent theory of call-by-value, i.e. theories in which not all terms are equals

Call-by-Value Separability and Computability

PAOLINI, LUCA LUIGI
First
2001-01-01

Abstract

The aim of this paper is to study the notion of separability in the call-by-value setting. Separability is the key notion used in the Böhm Theorem, proving that syntactically different βη-normal forms are separable in the classical λ-calculus endowed with β-reduction, i.e. in the call-by-name setting. In the case of call-by-value λ-calculus endowed with β v-reduction and η v-reduction (see Plotkin [7]), it turns out that two syntactically different βη v-normal forms are separable too, while the notion of β v-normal form and βη v-normal form is semantically meaningless. An explicit representation of Kleene’s recursive functions is presented. The separability result guarantees that the representation makes sense in every consistent theory of call-by-value, i.e. theories in which not all terms are equals
ICTCS 2001
Torino
2001
ICTCS 2001
Springer
2202
74
89
9783540426721
9783540454465
http://www.di.unito.it/~paolini/
https://link.springer.com/chapter/10.1007/3-540-45446-2_5
L. PAOLINI
File in questo prodotto:
File Dimensione Formato  
Call-by-Value Separability and Computability - LNCS 2001 ori.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 236.66 kB
Formato Adobe PDF
236.66 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Call-by-Value Separability and Computability - LNCS 2001 ori.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 236.66 kB
Formato Adobe PDF
236.66 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/8399
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? ND
social impact