Difference between revisions of "Exp3 8"

From The fun Wiki
Jump to navigation Jump to search
 
(One intermediate revision by the same user not shown)
Line 35: Line 35:
  
 
   main = put (toInt (pow n3 n8)) True;
 
   main = put (toInt (pow n3 n8)) True;
 +
 +
[[File:Exp38.png |600px|frameless]]
  
 
= Version 2 : Explicit Catamorphism =
 
= Version 2 : Explicit Catamorphism =

Latest revision as of 09:47, 8 August 2022

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;

Exp38.png

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.