0

I'm supposed to find normal form (if it exists) of following lambda term

(λy.y x (λx. y (λy.z) x)) v w

I understand first step of the process, which returns

(v x (λx.v (λy.z) x) w)

but i don't understand why this is given as final result of starting problem.

My question is: why can't i reduce that term further and have following as a result?

(v x (λx.v z) w)

Is there some specific rule that prevents me from doing that ?

Thanks

user3237206
  • 3

1 Answers1

3

By convention, in lambda calculus, terms associate from the left. Thus $$\lambda x. v (\lambda y. z) x$$ is to be interpreted as $$\lambda x. (v (\lambda y. z)) x$$ and NOT as $$\lambda x. v ((\lambda y. z) x)$$ Therefore you cannot apply the simplification $(\lambda y.z)x \to z$, which is what it looks like you were doing.

Ted
  • 33,788