Name: Anonymous 2008-02-10 16:09
I don't see the need for α-reduction in this instance:
Source: http://en.wikipedia.org/wiki/Y_combinator
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