Difference between revisions of "Exp3 8"
Jump to navigation
Jump to search
(Created page with "= Description = = The code = = Evaluation = == Reductions and Timing == == Garbage Collection ==") |
|||
| Line 1: | Line 1: | ||
= Description = | = Description = | ||
| − | + | Exp3_8 is a program from the nofib benchmark set that calculates 3^8 symbolically, using Church numbers. | |
| + | = Data Structures = | ||
| + | |||
| + | data Nat = Succ a | Zero; | ||
| + | data Bool = False | True ; | ||
| + | |||
| + | n1 = Succ Zero; | ||
| + | n2 = Succ(n1); | ||
| + | n3 = Succ(n2); | ||
| + | n4 = Succ(n3); | ||
| + | n5 = Succ(n4); | ||
| + | n6 = Succ(n5); | ||
| + | n7 = Succ(n6); | ||
| + | n8 = Succ(n7); | ||
| + | n9 = Succ(n8); | ||
| + | n10 = Succ(n9); | ||
| + | |||
| + | = Auxiliary Functions = | ||
| + | |||
| + | put x = out (extern 0x10a1fafa) x; | ||
| + | |||
| + | |||
| + | = Version 1 : Recursive = | ||
| + | |||
| + | add x y = x y (\a -> Succ (add a y)); | ||
| + | mul x y = y (Zero) (\a -> (add (mul x a) x)); | ||
| + | pow x y = y (Succ Zero) (\a -> mul x (pow x a)); | ||
| + | |||
| + | toInt n = n (0) (\a -> (+ 1 (toInt a))); | ||
| + | |||
| + | main = put (toInt (pow n3 n8)) True; | ||
| + | |||
| + | = Version 2 : Explicit Catamorphism = | ||
| + | fmap_nat f n = n Zero (\a -> Succ (f a )); | ||
| + | cata f alg x = alg (f (cata f alg) x); | ||
| + | natC z next = cata fmap_nat (\b -> b z (\a -> next a) ); | ||
| + | |||
| + | pow x y = natC (Succ Zero) (mul x) y; | ||
| + | add x y = natC y Succ x; | ||
| + | mul x y = natC Zero (add y) x; | ||
| + | |||
| + | toInt = cata fmap_nat (\x -> x 0 (+ 1)) ; | ||
| + | |||
| + | main = put (toInt (pows n3 n8)) True; | ||
| + | |||
| + | = Version 3 : Mendler-style Catamorphism = | ||
| + | natC z f = Fix (\s n -> n z (\a -> f (s a))); | ||
| + | |||
| + | pow x y = natC (Succ Zero) (mul x) y; | ||
| + | add x y = natC y Succ x; | ||
| + | mul x y = natC Zero (add y) x; | ||
| + | |||
| + | toInt = cata fmap_nat (\x -> x 0 (+ 1)) ; | ||
| + | |||
| + | main = put (toInt (pows n3 n8)) True; | ||
= Evaluation = | = Evaluation = | ||
| Line 8: | Line 62: | ||
== Reductions and Timing == | == Reductions and Timing == | ||
| − | + | ||
| + | {| | ||
| + | !header1 !! header2 | ||
| + | |- | ||
| + | |row1 cell1 || cell2 | ||
| + | |- | ||
| + | |row2 cell1 || cell2 | ||
| + | |} | ||
Revision as of 03:39, 28 July 2022
Description
Exp3_8 is a program from the nofib benchmark set that calculates 3^8 symbolically, using Church numbers.
Data Structures
data Nat = Succ a | Zero; data Bool = False | True ; n1 = Succ Zero; n2 = Succ(n1); n3 = Succ(n2); n4 = Succ(n3); n5 = Succ(n4); n6 = Succ(n5); n7 = Succ(n6); n8 = Succ(n7); n9 = Succ(n8); n10 = Succ(n9);
Auxiliary Functions
put x = out (extern 0x10a1fafa) x;
Version 1 : Recursive
add x y = x y (\a -> Succ (add a y)); mul x y = y (Zero) (\a -> (add (mul x a) x)); pow x y = y (Succ Zero) (\a -> mul x (pow x a));
toInt n = n (0) (\a -> (+ 1 (toInt a)));
main = put (toInt (pow n3 n8)) True;
Version 2 : Explicit Catamorphism
fmap_nat f n = n Zero (\a -> Succ (f a )); cata f alg x = alg (f (cata f alg) x); natC z next = cata fmap_nat (\b -> b z (\a -> next a) );
pow x y = natC (Succ Zero) (mul x) y; add x y = natC y Succ x; mul x y = natC Zero (add y) x; toInt = cata fmap_nat (\x -> x 0 (+ 1)) ;
main = put (toInt (pows n3 n8)) True;
Version 3 : Mendler-style Catamorphism
natC z f = Fix (\s n -> n z (\a -> f (s a))); pow x y = natC (Succ Zero) (mul x) y; add x y = natC y Succ x; mul x y = natC Zero (add y) x; toInt = cata fmap_nat (\x -> x 0 (+ 1)) ;
main = put (toInt (pows n3 n8)) True;
Evaluation
Reductions and Timing
| header1 | header2 |
|---|---|
| row1 cell1 | cell2 |
| row2 cell1 | cell2 |