Normal form Lambda calculus expression

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.

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

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

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

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.
{"ft_lang_label":"__label__en","ft_lang_prob":0.89322084,"math_prob":0.9968223,"size":597,"snap":"2019-43-2019-47","text_gpt3_token_len":158,"char_repetition_ratio":0.19224283,"word_repetition_ratio":0.0,"special_character_ratio":0.2680067,"punctuation_ratio":0.13432837,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99928385,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-21T17:53:07Z\",\"WARC-Record-ID\":\"<urn:uuid:313a0d72-497c-4ad8-9a56-7c8f44576bd0>\",\"Content-Length\":\"135121\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:2c2291dc-63db-4cc1-85ff-583a594a38d6>\",\"WARC-Concurrent-To\":\"<urn:uuid:92e33e39-d29e-4667-96e2-27ce2f5c28b3>\",\"WARC-IP-Address\":\"151.101.1.69\",\"WARC-Target-URI\":\"https://cs.stackexchange.com/questions/12268/normal-form-lambda-calculus-expression\",\"WARC-Payload-Digest\":\"sha1:QMWNJSTJQJSS32YL2GQIYUMXCWGOV332\",\"WARC-Block-Digest\":\"sha1:TTRXEC5YAJ6FCLXDS5TWEMYUUM5PKU3I\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570987781397.63_warc_CC-MAIN-20191021171509-20191021195009-00389.warc.gz\"}"}