1 -> (s (0));


neg (neg ?x) -> ?x;
neg (0)      -> 0;


add (s ?x) (s ?y) -> s (add ?x (s ?y));
add (0)    (s ?x) -> s ?x;
add (s ?x) (0)    -> s ?x;
add (0)    (0)    -> 0;


?x + ?y + ?z -> (?x + ?y) + ?z;


?x + ?y -> add ?x ?y;


sub (s ?x) (s ?y) -> sub ?x ?y;
sub (s ?x) (0)    -> s ?x;
sub (0)    (s ?x) -> neg (s ?x);
sub (0)    (0)    -> 0;


?x - ?y -> sub ?x ?y;


mul (s ?x) (s ?y)  -> (s ?x) + (mul (s ?x) ((s ?y) - 1));
mul (s ?x) (s (0)) -> s ?x;
mul (s ?x) (0)     -> 0;
mul (0)    (s ?x)  -> 0;


?x * ?y -> mul ?x ?y;


Ensures that a list or a number has been reduced to its normal form. ;

reduced (0)       -> true;
reduced (nil)     -> true;
reduced (s ?x)    -> reduced ?x;
reduced (?h : ?t) -> reduced ?t;
reduced ?x        -> false;


Because there may be conflicts with expressions that
are currently being reduced, we need to fold over reduced
lists, i.e ones that have already been fully generated. ;

fold       (?f) ?i ?l           -> fold reduced ?l (?f) ?i ?l;
fold true  (?f) ?i (nil)        -> ?i;
fold true  (?f) ?i (?h : (nil)) -> ?f ?i ?h;
fold true  (?f) ?i (?h : ?t)    -> ?f ?i (fold (?f) ?h ?t);
fold false (?f) ?i ?l           -> fold (?f) ?i ?l;


factorial (s (0)) -> s (0);
factorial (s ?x)  -> (s ?x) * (factorial ((s ?x) - 1));


sum (?h : ?t) -> fold (add) (0) (?h : ?t);


range ?x (s (0)) -> ?x : (nil);
range ?x (s ?y)  -> ?x : (range (?x + 1) ((s ?y) - 1));


Disgusting (yet valid) hack for currying.
We need lambdas. ;

unpack (?h : nil) -> ?h;
unpack (?h : ?t)  -> ?h unpack ?t;
unpack (?x)       -> ?x;
unpack (?x .      -> ?x unpack (;


:: (?f) ?a -> ?f unpack ?a;


mapp (?f) ?a (nil)        -> nil;
mapp (?f) ?a (?h : (nil)) -> (?f unpack ?a ?h) : (nil);
mapp (?f) ?a (?h : ?t)    -> (?f unpack ?a ?h) : (mapp (?f) ?a ?t);


map (?f) (nil)      -> nil;
map (?f) (?h : nil) -> (?f ?h) : (nil);
map (?f) (?h : ?t)  -> (?f ?h) : (map (?f) ?t);


product ?x -> fold (mul) 1 ?x;


factorial2 ?x -> product (range 1 ?x);


contains ?x (nil)     -> false;
contains ?x (?x : ?t) -> true;
contains ?x (?h : ?t) -> contains ?x ?t;


unique       (nil)     -> nil;
unique false (?h : ?t) -> ?h : (unique ?t);
unique true  (?h : ?t) -> unique ?t;
unique       (?h : ?t) -> unique contains ?h ?t (?h : ?t);


length (nil)     -> 0;
length (?h : ?t) -> s (length ?t);


zipWith (?f) (nil)       (nil)       -> nil;
zipWith (?f) (?h : ?t)   (nil)       -> nil;
zipWith (?f) (nil)       (?h : ?t)   -> nil;
zipWith (?f) (?h1 : ?t1) (?h2 : ?t2) -> (?f ?h1 ?h2) : (zipWith (?f) ?t1 ?t2);


evens ?x -> zipWith (add) (range (0) ?x) (range (0) ?x);


not (not ?x) -> ?x;
not true     -> false;
not false    -> true;


any ?x -> contains true ?x;


all ?x -> not contains false ?x;


none ?x -> not any ?x;


add1 ?x -> add ?x 1;


square ?x -> ?x * ?x;


reduce (s ?x)    -> s (reduce ?x);
reduce (0)       -> (0);
reduce (?h : ?t) -> ?h : (reduce ?t);
reduce (nil)     -> nil;