1
$\begingroup$

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!

$\endgroup$
1
  • 1
    $\begingroup$ You bracket the expression (correctly) as application being left-associative, but write right-associative. $\endgroup$
    – funkstar
    Dec 27, 2011 at 23:14

1 Answer 1

9
$\begingroup$

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)$.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.