<h2>Background</h2>
<p>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):<span class="math-container">$$T\text{ solvable} \overset{\text{def}}{=}\forall N,\exists K,K[T]\to^*N\land \lnot \forall U,K[U]\to ^*N$$</span>and the simplified one, which is far more common, states that it can be used as an operator to get the identity:<span class="math-container">$$T\text{ solvable} \overset{\text{def}}{=}\exists H,H[T]\to^*I$$</span>where <span class="math-container">$H$</span> ranges over contexts of the shape <span class="math-container">$(\lambda x_1.\dots .\lambda x_q.\square) t_1\dots t_r$</span> (that close the term <span class="math-container">$T$</span>), and <span class="math-container">$I=\lambda x.x$</span> is the identity.</p>
<p>I will call the first definition K-N-solvability and the second H-I-solvability.</p>
<h2>Question</h2>
<p>In the paper Call-by-value solvability, the equivalence between K-N-solvability and H-I-solvability is said to mean that &quot;<span class="math-container">$\lambda$</span>-terms have functional behavior&quot; (second half of p. 508). It is then said that the call-by-value <span class="math-container">$\lambda$</span>-calculus also has functional behavior, and that it is therefore reasonable to use H-I-solvability in the call-by-value <span class="math-container">$\lambda$</span>-calculus.</p>
<p>I am under the impression that both definitions of solvability are not equivalent in the call-by-value <span class="math-container">$\lambda$</span>-calculus. The term <span class="math-container">$\lambda x.\Omega$</span> with <span class="math-container">$\Omega =(\lambda x_1.x_1x_1)(\lambda x_2.x_2x_2)$</span> not H-I-solvable, but seems to be K-N-solvable since <span class="math-container">$K=(\lambda y.I)[]$</span> is such that <span class="math-container">$K[\lambda x.\Omega]\to I$</span> and <span class="math-container">$K[\Omega]$</span> can not reduce to a normal form because it can only reduce to itself (because we are in call-by-value).</p>
<ul>
<li><p>Did I miss something?</p>
</li>
<li><p>If not, is this written somewhere I could cite?</p>
</li>
</ul>
<p>(I also think that K-N-solvability is equivalent to what the authors call potential valuability)</p>

CC BY-SA 4.0
2022-04-06T03:09:27.727Z
A relevant reference should be García-Pérez and Nogueira: No solvable lambda-value term left behind.
pbaren
CC BY-SA 4.0
2022-04-06T10:33:47.347Z
@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.
xavierm02
CC BY-SA 4.0
2022-04-06T10:43:44.303Z
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.
xavierm02
CC BY-SA 4.0
2022-04-19T16:21:37.247Z
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.
Beniamino Accattoli
CC BY-SA 4.0
2022-04-22T11:21:16.753Z
@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)
xavierm02
<lambda-calculus>
Call-by-value solvability
xavierm02
# Call-by-value solvability

(Asked by: username_0 on 2022-04-01)

## 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)

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: A relevant reference should be García-Pérez and Nogueira: No solvable lambda-value term left behind.  
> **username_0**: @username_1 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.  
> **username_0**: 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.  
> **username_2**: 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.  
> **username_0**: @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)  

---

## 0 answers

