Call-by-Value Separability and Computability

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