Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

Why does α-reduction occur?

Name: Anonymous 2008-02-10 16:09

I don't see the need for α-reduction in this instance:

Y g = (λf . (λx . f (x x)) (λx . f (x x))) g
Y g = (λx . g (x x)) (λx . g (x x))              (β-reduction of λf - applied main function to g)
Y g = (λy . g (y y)) (λx . g (x x))              (α-conversion - renamed bound variable)
Y g = g ((λx . g (x x)) (λx . g (x x)))          (β-reduction of λy - applied left function to right function)
Y g = g (Y g)                                    (definition of Y)


Source: http://en.wikipedia.org/wiki/Y_combinator

Name: Anonymous 2008-02-10 18:12

α-conversion exists to stop free-variable capture in β-reduction. In (λx.λy.y x) (λz.y), α-conversion is necessary to change the ys to some other symbol, so as not to conflict with the free-variable in (λz.y) which would cause the wrong output, λy.y (λz.y). A correct output is λk.k (λz.y), or even λz.z (λz.y).

Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List