Description

Exp3_8 is a program from the nofib benchmark set that calculates 3^8 symbolically, using Church numbers.

The source code for Version 1 is available on github.

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;
  
  main = put (toInt (pows n3 n8)) True;

Evaluation

Reductions and Timing

	Recursive	Catamorphism	Mendler-style
Reductions	16175369	492059	314921
Traversal steps	40400688	1053012	692175
Node Allocations	40367860	925075	524872
Total cycles*	88900524	2214275	1505722

\*Total cycle count include operations that take CPU time but are not considered combinators, such as links, i/o and garbage collection. This reference value was obtained with a development version of the Blackbird CPU.

Exp3 8

Contents