CODEWITHSUNDEEP
lambda-calculus
vauge
vauge

Reputation: 801

Lambda calculus - why isn't it possible to make another beta reduction here?

I have been told that the term 

(z (λy.z x) (λy.y z))

is already in it's normal form - but I don't understand why. Couldn't one make another beta-reduction in this state and replace all occurences of y in the term (λy.z x) by (λy.y z), so that it would evaluate to:

(z (λy.z x) (λy.y z)) ==> (z z x)

Upvotes: 3

Views: 96

Answers (1)

user395760
user395760

Reputation:

Application is generally taken to be left-associative. That is,

z (λy.z x) (λy.y z)

is not

z ((λy.z x) (λy.y z))

It is

(z (λy.z x)) (λy.y z)

which would require the value of z to beta-reduce.

Upvotes: 3

Related Questions