0
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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$.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.