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)

  • 1
    $\begingroup$ How is λz.λz (z z) t parsed? Is it λz.(λz (z z) t) or (λz.λz (z z)) t? $\endgroup$ Jun 23 '15 at 13:55
  • $\begingroup$ it is (λz.λz (z z)) t $\endgroup$ Jun 26 '15 at 13:03
  • $\begingroup$ 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)$. $\endgroup$ Jun 26 '15 at 13:07

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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