Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (\g.\f.\x. g f (f x)) (\f.\x. x)
- (\g. \f0. \x0. g f0 (f0 x0)) (\f1. \x1. x1) -- alpha rename to avoid collisions
- \f0. \x0. (\f1. \x1. x1) f0 (f0 x0) -- apply parameter for g
- g = (\f1. \x1. x1)
- \f0. \x0. f0 x0 -- apply parameters to inner lambda and reduce
- f1 = f0
- x1 = f0 x0
- reduction of (\f1. \x1. x1) eliminates f1 and produces x1
- one can now further note that the above is essentially id, because it takes
- f0 x0 and produces f0 x0
Add Comment
Please, Sign In to add comment