Frage

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.

War es hilfreich?

Lösung

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.

Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit StackOverflow
scroll top