﻿

# 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);
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