Question

say I have the following example of a lambda expression with \x meant to represent lambda x

What would the beta reduction of the following be?

(\x.\x.(x x)) \z.z

My first instinct would have been for this to be

\x.(\z.z \z.z)

But someone I spoke with was of the opinion that the second \x would also be replaced with \z.z

which would mean it is really

\(\z.z).(\z.z \z.z) 

Can someone please clarify what the correct approach would be. I can't say I really understand the second approach.

Was it helpful?

Solution

Actually, (\x.\x.(x x)) \z.z is alpha equivalent to (\x.\y.(y y)) \z.z because variables are always bound to the closest lambda abstraction.

This means (\x.\x.(x x)) \z.z is beta equivalent to \x.(x x).

Substitution is never done on lambda abstractions, the \x. part.

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top