3
$\begingroup$

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)

Improve this question
$\endgroup$
5
  • 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$
    – Beniamino Accattoli
    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

0

Reset to default

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.