# Call-by-value solvability

## Background

There are two fairly common definitions of solvability. The general one states that the term can be used to get any chosen result (i.e. normal form):$$T\text{ solvable} \overset{\text{def}}{=}\forall N,\exists K,K[T]\to^*N\land \lnot \forall U,K[U]\to ^*N$$and the simplified one, which is far more common, states that it can be used as an operator to get the identity:$$T\text{ solvable} \overset{\text{def}}{=}\exists H,H[T]\to^*I$$where $$H$$ ranges over contexts of the shape $$(\lambda x_1.\dots .\lambda x_q.\square) t_1\dots t_r$$ (that close the term $$T$$), and $$I=\lambda x.x$$ is the identity.

I will call the first definition K-N-solvability and the second H-I-solvability.

## Question

In the paper Call-by-value solvability, the equivalence between K-N-solvability and H-I-solvability is said to mean that "$$\lambda$$-terms have functional behavior" (second half of p. 508). It is then said that the call-by-value $$\lambda$$-calculus also has functional behavior, and that it is therefore reasonable to use H-I-solvability in the call-by-value $$\lambda$$-calculus.

I am under the impression that both definitions of solvability are not equivalent in the call-by-value $$\lambda$$-calculus. The term $$\lambda x.\Omega$$ with $$\Omega =(\lambda x_1.x_1x_1)(\lambda x_2.x_2x_2)$$ not H-I-solvable, but seems to be K-N-solvable since $$K=(\lambda y.I)[]$$ is such that $$K[\lambda x.\Omega]\to I$$ and $$K[\Omega]$$ can not reduce to a normal form because it can only reduce to itself (because we are in call-by-value).

• Did I miss something?

• If not, is this written somewhere I could cite?

(I also think that K-N-solvability is equivalent to what the authors call potential valuability)

• A relevant reference should be García-Pérez and Nogueira: No solvable lambda-value term left behind. Apr 6, 2022 at 3:09
• @pbaren From what I understand, the main point of this paper is that $\forall N, F[T] \to^*N$ (which should be equivalent to H-I-solvable) is not equivalent to $\exists N, F[T] \to^*N$ (where function contexts $F$ have the same shape as head contexts $H$ but are allowed to be open) and that using an existential quantification (and allowing open terms) yields a better notion of operational relevance. In particular, they seem to not discuss definitions with arbitrary contexts $K$ (e.g. K-N-solvability) in the call-by-value $\lambda$-calculus. Apr 6, 2022 at 10:33
• They also cite the paper "Operational, denotational and logical descriptions: a case study" (which is also cited in "Call-by-value solvability", where they point to Thm 33), but it is unclear to me how this relates to the equivalence between H-I-solvability and K-N-solvability. Apr 6, 2022 at 10:43
• I guess that, in cbv, the U in K-N-solvability must be a value. This should make the two notions equivalent (or at least rule out your counter-example). Careful with what you say at the end: H-I-solvability is not equivalent to potential valuability, this is well known, the typical example being $\lambda x.\Omega$, which is potentially valuable (because it is a value) but not cbv-solvable. Apr 19, 2022 at 16:21
• @BeniaminoAccattoli The idea of restricting what $U$ ranges over is very interesting. Restricting to values might not work (e.g. $T=\lambda x.\lambda y.\Omega$ looks K-N-solvable thanks to $K=(\lambda z.I)(\square V)$, even with $U$ restricted to values), but it looks likely that some restriction works. (About the equivalence with potential valuability, I meant K-N-solvability, not H-I-solvability. I edited the question) Apr 22, 2022 at 11:21