Why is this lambda calculus expression already in normal form?

109 Views Asked by At

I don't quite follow why the following expression is in normal form

$$\lambda y.(y (\lambda z.w) (\lambda z.w))$$

I would have thought that reduces to $\lambda y.y w$, but according to http://www.itu.dk/people/sestoft/lamreduce/lamframes.html it is already in normal form.

Can someone explain that to me?

1

There are 1 best solutions below

0
On BEST ANSWER

The expression $(a\, b\, c)$ is short for $((a\, b)\, c)$, not for $(a\, (b\, c))$. In $(( a\, b)\, c)$ the subexpression $b$ is not being applied to $c$.

In your example, you have $(y\, (\lambda z.w)\, (\lambda z.w))$. If it were $(y\; \color{darkred}{((\lambda z.w) (\lambda z.w))})$ you could reduce it as you suggest. But it isn't that; it is $(\color{darkred}{(y (\lambda z.w))}\; (\lambda z.w))$, which is different.

One way to think of $(a\,b\,c)$ is that $a$ is a function of two arguments, which are $b$ and $c$. You cannot reduce this expression without knowing what function $a$ is, and you cannot reduce it by applying one argument to the other argument.

For example, with suitable definitions of $plus, 2, 3, $ and $5$, we have $(plus\, 2\, 3)\Rightarrow 5$. It does not make sense to try to reduce this by first applying $2$ to $3$.