Guest User

Untitled

a guest
Jan 21st, 2019
74
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.44 KB | None | 0 0
  1. (\g.\f.\x. g f (f x)) (\f.\x. x)
  2.  
  3. (\g. \f0. \x0. g f0 (f0 x0)) (\f1. \x1. x1) -- alpha rename to avoid collisions
  4.  
  5. \f0. \x0. (\f1. \x1. x1) f0 (f0 x0) -- apply parameter for g
  6. g = (\f1. \x1. x1)
  7.  
  8. \f0. \x0. f0 x0 -- apply parameters to inner lambda and reduce
  9. f1 = f0
  10. x1 = f0 x0
  11. reduction of (\f1. \x1. x1) eliminates f1 and produces x1
  12.  
  13. one can now further note that the above is essentially id, because it takes
  14. f0 x0 and produces f0 x0
Add Comment
Please, Sign In to add comment