Lambda calculus Beta reduction

Question

When applying Beta reduction does the function also affect on the $\lambda$ term? (If same value)

For example

$\lambda$ z.$\lambda$ z (z z) t

What is the correct reduction?

$\lambda$z (t t) or

$\lambda$t (t t)

How is λz.λz (z z) t parsed? Is it λz.(λz (z z) t) or (λz.λz (z z)) t? — Daniel Fischer, Jun 23 '15 at 13:55
Then you get $\lambda u, (u; u)$. Of course instead of $u$, you can call the variable anything you like, e.g. $t$ or $z$. Note that $\lambda z., \lambda z, (z; z) \equiv \lambda z., \lambda y, (y; y)$. — Daniel Fischer, Jun 26 '15 at 13:07

score 0 · Answer 1 · answered Mar 31 '16 at 13:53

The beta contraction of $(\lambda x . M)\, N$ is defined as $[N/x]\, M$, and recall that the substitution is done by replacing every free instance of $x$ by $N$.

Explicitly, $(\lambda z. (\lambda z. zz))t \triangleright_\beta [t/z]\,(\lambda z. zz)$, but as there is no free occurence of $z$ no substitution is performed.

Lambda calculus Beta reduction

1 Answers1