<p>The expression $x(\lambda y.P)z$ is not $\beta$-reducible (unless there is a redex inside $P$, that is, but no such reduction sequence can escape outside the $\lambda$). The reduction you mention is invalid even in $\lambda\eta$-calculus. The only explanation I can imagine is that the expression in your derivation was misbracketed, and should actually read $x((\lambda y.P)z)$.</p>

CC BY-SA 3.0
2011-12-22T12:44:56.770Z
2011-12-22T12:44:56.770Z
Emil Jeřábek
<p>Consider the untyped $\lambda$-calculus expression</p>

<p>$$x(\lambda y.P\;)z$$</p>

<p>...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex.  Can this expression be $\beta$-reduced?  I've consulted several textbooks, but they are all silent on this point (as far as I can tell).  Application is left-associative, so the fully-parenthesized rendition of the expression above would be</p>

<p>$$((x(\lambda y.P\;))z)$$</p>

<p>The formalism, as given in all the textbooks I've consulted, specifies a $\beta$-reduction for $((\lambda y.P\;)z)$, namely $((\lambda y.P\;)z)\; \triangleright_{\beta} \;([z/y]P\;)$, but not one for $((x(\lambda y.P\;))z)$.  Therefore, the answer to my question would appear to be "no", but a derivation I'm working my way through seems to require an invalid-looking $\beta$-reduction of the form</p>

<p>$$((x(\lambda y.P\;))z) \;\; \triangleright_{\beta} \;\;(x([z/y]P\;))\;.$$</p>

<p>Any help with this would be appreciated.  In particular, reference to a treatment of the $\lambda$-calculus that explicitly adjudicates this question would be very helpful.  Thanks!</p>

CC BY-SA 3.0
2011-12-27T23:14:23.890Z
You bracket the expression (correctly) as application being left-associative, but write right-associative.
funkstar
<lo.logic><lambda-calculus>
Can "$x(\lambda y.P\;)z$" be $\beta$-reduced?
kjo
# Can "$x(\lambda y.P\;)z$" be $\beta$-reduced?

(Asked by: username_0 on 2011-12-22)

Consider the untyped $\lambda$-calculus expression

$$x(\lambda y.P\;)z$$

...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've consulted several textbooks, but they are all silent on this point (as far as I can tell). Application is left-associative, so the fully-parenthesized rendition of the expression above would be

$$((x(\lambda y.P\;))z)$$

The formalism, as given in all the textbooks I've consulted, specifies a $\beta$-reduction for $((\lambda y.P\;)z)$, namely $((\lambda y.P\;)z)\; \triangleright\_{\beta} \;([z/y]P\;)$, but not one for $((x(\lambda y.P\;))z)$. Therefore, the answer to my question would appear to be "no", but a derivation I'm working my way through seems to require an invalid-looking $\beta$-reduction of the form

$$((x(\lambda y.P\;))z) \;\; \triangleright\_{\beta} \;\;(x([z/y]P\;))\;.$$

Any help with this would be appreciated. In particular, reference to a treatment of the $\lambda$-calculus that explicitly adjudicates this question would be very helpful. Thanks!

**Tags:** lo.logic, lambda-calculus
> **Comments:**
> **username_1**: You bracket the expression (correctly) as application being left-associative, but write right-associative.  

---

## 1 answers

### Answer by username_2 on 2011-12-22. Score: 9 | Accepted answer

The expression $x(\lambda y.P)z$ is not $\beta$-reducible (unless there is a redex inside $P$, that is, but no such reduction sequence can escape outside the $\lambda$). The reduction you mention is invalid even in $\lambda\eta$-calculus. The only explanation I can imagine is that the expression in your derivation was misbracketed, and should actually read $x((\lambda y.P)z)$.


---

