Guest User

Untitled

a guest
Feb 11th, 2014
130
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. sum (take (s (s (s (s (s z))))) (cycle (take (s (s (s z))) (filter (leq (s z)) nats)))) where
  2. id = \x. x;
  3. force = \thunk. thunk _;
  4. fix = \f. (\x. f (\y. x x y)) (\x. f (\y. x x y));
  5.  
  6. true = \p _. p;
  7. false = \_ q. q;
  8. or = \p q. p p q;
  9. if = id;
  10.  
  11. z = \_ z. z;
  12. s = \n s z. s (n s z);
  13. eq0 = \n. n (\_. false) true;
  14. plus = \m n s z. m s (n s z);
  15. pred = \n s z. n (\g h. h (g s)) (\_. z) (\x. x);
  16. sub = \n m. m pred n;
  17. leq = \n m. eq0 (sub n m);
  18.  
  19. nil = \ _ z. z;
  20. cons = \x xs f z. f (\_. x) (\f' _. xs f' z);
  21. consC = \x xs f z. f x (\f' _. xs f' z);
  22. tail = \xs f z. xs (\_ r. force (r f)) z;
  23. foldr = \f z xs. xs (fix (\rec f x r. f x (r (rec f))) f) z;
  24. defhead = foldr (\x _. force x);
  25. head = defhead _;
  26. null = foldr (\_ _. false) true;
  27.  
  28. ifNull = \xs def f. if (null xs) def (\_. force (f xs));
  29. ifNullNil = \xs. ifNull xs nil;
  30. append = fix (\append xs1 xs2. ifNull xs1 xs2
  31. (\xs1. consC (\_. head xs1) (append (tail xs1) xs2)));
  32. map = fix (\map f xs. ifNullNil xs
  33. (\xs. consC (\_. f (head xs)) (map f (tail xs))));
  34. take = fix (\take n xs. if (eq0 n) nil (ifNullNil xs
  35. (\xs. consC (\_. head xs) (take (pred n) (tail xs)))));
  36. filter = fix (\filter p xs. ifNullNil xs
  37. (\xs. if (p x)
  38. (cons x (filter p (tail xs)))
  39. (filter p (tail xs))
  40. where x = head xs.));
  41. cycle = fix (\cycle xs. \_. force (append xs (cycle xs)));
  42.  
  43. s1foldr = \f. foldr (\x acc. f x (force acc));
  44. s2foldr = \f. foldr (\x acc. f (force x) acc );
  45. sfoldr = \f. foldr (\x acc. f (force x) (force acc));
  46.  
  47. nats = fix (\rec n. \_. force (cons n (rec (s n)))) z;
  48. sum = sfoldr plus z.
  49.  
  50. result: \s z. s (s (s (s (s (s (s (s (s z))))))))
  51. equals to haskell "sum $ take 5 $ cycle $ take 3 $ filter (1 <=) [0..]" --> 1 + 2 + 3 + 1 + 2 = 9
RAW Paste Data