Title Call-By-Value Separability and Computability
Authors Luca Paolini, DISI-Università di Genova & IML-Université de la Méditerranée
Main Fields 3. computability
9. foundations of functional programming
22. semantics of programming
Other Main Fields
Abstract + Keywords \section{Abstract}

In this paper the notion of separability is studied 
in the call-by-value setting. 
The separability is the key notion used in the B\"ohm-theorem, 
proving that syntactically different $\beta\eta$-normal forms are separable 
in the classical $\lambda$-calculus endowed with the $\beta$-reduction,
i.e. in the call-by-name setting. 

In the call-by-value $\lambda$-calculus (see Plotkin [7])
endowed with the $\beta_v$-reduction and the $\eta_v$-reduction,
it turns out that two syntactically different $\beta\eta$-normal forms 
are separable too, while the notion of $\beta_v$-normal form and
$\eta_v$-normal form are not relevant for separability.

This separability result is then used for building 
an explicit representation 
of the Kleene's recursive functions. 

Keywords: call-by-value, $\lambda$-calculus, separability,
computability.