문제

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.

도움이 되었습니까?

해결책

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.

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 StackOverflow
scroll top