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.


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)

  • 1
    $\begingroup$ A relevant reference should be García-Pérez and Nogueira: No solvable lambda-value term left behind. $\endgroup$
    – pbaren
    Apr 6 at 3:09
  • $\begingroup$ @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. $\endgroup$
    – xavierm02
    Apr 6 at 10:33
  • $\begingroup$ 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. $\endgroup$
    – xavierm02
    Apr 6 at 10:43
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 19 at 16:21
  • $\begingroup$ @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) $\endgroup$
    – xavierm02
    Apr 22 at 11:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.