Beta reduction on $(\lambda x . xu)(\lambda z. wzwz)yv$

Question

I need to perform a reduction on the following lambda expression

$(\lambda x . xu)(\lambda z. wzwz)yv$

This is what I have done so far:

$(\lambda x . xu)(\lambda z. wyvwyv) = wyvwyvu$

However, my workbook has done it a bit differently. They used the following steps:

$(\lambda x . xu)(\lambda z. wzwz)yv$ = $((\lambda z. wzwz)u)yv = wuwuyv $

My question is: Are both of these reductions valid? It seems they first applied $(\lambda x. xu)$ to $(\lambda z. wzwz)$, and, on the other hand, I first applied $(\lambda z. wzwz$ to $yv$.

Provided that both are correct, it's obvious that their solution is a bit shorter. Is there any way I can "know" which steps to take so they lead me to the shortest expression?

Answer 1

No, they are not both valid. The problem is that lambda-calculus is not associative, hence

$$(\lambda x.xu)((\lambda z.wzwz)(yv)) \neq (\lambda x.xu)((\lambda z.wzwz))(yv).$$

If you calculate the first one, you get your result, hence

$$(\lambda x.xu)((\lambda z.wzwz)(yv))=(\lambda x.xu)(wyvwyv)=wyvwyvu;$$

while if you calculate the second one, you get your book's result, that is

$$(\lambda x.xu)((\lambda z.wzwz))(yv)=((\lambda z.wzwz)u)(yv)=wuwuyv.$$

These are different results. Clearly it depends on how the parentheses are put. I'm not a type theorist myself, but if I recall correctly they associate lambdas to the left and other terms to the right (as your book does).

EDIT: yeah I wrote $=$ instead of $\to_\beta$, but again I'm not a type theorist so I don't recall perfectly every detail of the notation, sorry

Answer 2

It looks like the author of your workbook has been a little bit lazy about conventions for omitting brackets. In the $\lambda$-calculus, an expression like $f\,x\,y$ is ambiguous: it could mean $(f\,x)\,y$ or $f\,(x\, y)$. The first of these readings (which can be described by saying that "function application is left-associative") is the one most commonly used. If you follow the left-associative reading, you will get the same result as your workbook, but you have chosen the right-associative reading giving a different result.