1
$\begingroup$

I need a little help with a lambda calculus reduction to normal form: $$(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)$$ It should be solved like this: $$xx(\lambda x.x)y((\lambda x.x)x)$$ and then: $$xx(\lambda x.x)y(x)$$

This is the result of any of the lambda calculators that you can find online.

My question is: why can't I go on with reductions and make also $(\lambda x.x)y$ so the resulting expression would be $xxy(x)$?

Can you give me a complete answer, with theory of lambda calculus rules/proofs?

I really want to understand this exercise, any help would be appreciated.

$\endgroup$

migrated from cstheory.stackexchange.com May 25 '13 at 11:46

This question came from our site for theoretical computer scientists and researchers in related fields.

  • 1
    $\begingroup$ I think your first term is broken. There are too many x's before the first dot. (Also, migrating to Computer Science.) $\endgroup$ – Dave Clarke May 25 '13 at 11:46
2
$\begingroup$

As pointed out in the comments, the first term seems broken - too many $x$es.

The key is that function application is not associative (both in the lambda calculus and outside it). In particular, $a(bc)$ is different from $(ab)c$. In the first term, we apply $b$ to $c$ and then $a$ to the result. In the second term, we apply $a$ to $b$ and then apply the result on $c$.

In your case $xx(\lambda x.x)yx$ is parenthesised as $(((xx)(\lambda x.x))y)x$, because function application associates to the left. This means that there is no redex there, it can't be reduced further.

Your mistake was in that you added parentheses like $xx((\lambda x.x)y)x$, which is a completely different term.

$\endgroup$

Your Answer

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