0
$\begingroup$

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)

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

1 Answer 1

Reset to default
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.