


//          Standard Functions for the plc interpreter for the
//        pure lambda calculus by Viktor "AlgorithMan" Engelmann
//                     http://www.AlgorithMan.de





// #######################################################################
// ####################### Functions for Arithmetic ######################
// #######################################################################

zero = λf.λx.x ;
succ = λn.λf.λx.f (n f x) ;
add = λn.n succ ;
mult = λn.λm. n (m succ) zero ;
pred = λn.λf.λx. (n (λg.λh.h(g f)) (λu.x)) (λu.u) ;
sub = λn.λm.m pred n ;





// #######################################################################
// #################### Functions for Boolean Algebra ####################
// #######################################################################

true = λx.λy.x ;
false = λx.λy.y ;
if = λb.λt.λe.b t e ;
or = λx.x true;
and = λx.λy.x y false;
not = λx.λa.λb.x b a ;





// #######################################################################
// ####################### Functions for Relations #######################
// #######################################################################

iszero = λn.n (λp.false) true ;
ge = λn.λm.iszero (sub m n) ;
gt = λn.λm.and (ge n m) (not (ge m n)) ;
eq = λn.λm.and (ge m n) (ge n m) ;
neq = λn.λm.not (eq n m);
lt = not gt ;
le = not ge ;





// #######################################################################
// ####################### Functions for Recursion #######################
// #######################################################################

// Alonzo Church's Fixpoint Combinator
fix = (λx.λy.y (x x y)) (λx.λy.y (x x y)) ;

// e.g. my (λx.iszero (sub 5 x));  =  5
//      my (λx.iszero (sub 9 (mult x x)));  =  3
my = fix (λs.λn.λphi.(phi n)
                         n
                         (s (succ n) phi)
         ) 0 ;
         
fact = fix (λf.λn. (iszero n)
                       1
                       (mult n (f (pred n)))
           );
fibo = fix (λf.λn. (iszero (pred (pred n)))
                       1
                       (add   (f (pred n))   (f (pred (pred n))) )
           ) ;





// #######################################################################
// ######################### Functions for lists #########################
// #######################################################################

pair = λy1.λy2.λf.f y1 y2;

first = λg.g(λy1.λy2.y1);

second = λg.g(λy1.λy2.y2);

nil = λx.true;

isnil = λp. p (λx.λy.false);

fold = fix (λf.λp.λq.λl. (isnil l)
                             q
                             (p   (first l)   (f p q (second l)))
           );

// e.g.  map succ (pair 3 (pair 4 (pair 7 nil)));  =  [4,5,8]
map = λf.fold (λx.pair (f x)) nil;
          
// e.g. length (pair 3 (pair 4 (pair 7 nil)));  =  3
length = fold (λx.succ) 0;

// e.g.  listsum (pair 3 (pair 4 (pair 7 nil)));  =  14
listsum = fold add 0;





// #######################################################################
// ######################### Functions for trees #########################
// #######################################################################

// e.g.  treenodes (pair (pair nil nil) (pair nil nil));  =  3
treenodes = fix (λn.λx. ((isnil x)
                            0
                            (succ    (add (n (first x))  (n (second x)) ))
                        )
                );
                
// e.g.  treeleafs (pair (pair nil nil) (pair nil nil));  =  2
treeleafs = fix (λl.λx. ((isnil x)
                              0 
                              ((and   (isnil (first x))   (isnil (second x)))
                                  1
                                  (add   (l (first x))   (l (second x))   ) 
                              ) 
                        )
                );

























