// Programming with pure lambda terms, with full beta and weak head reduction
// default define means reduce defined term to weak-head normal form.
define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.(x z (y z));
define True = K;
define False = (K I);
define IF = lambda b.lambda x.lambda y.(b x y);
define NOT = lambda b.(IF b False True);
define OR = lambda a.lambda b.(IF a True b);
define AND = lambda a.lambda b.(IF a b False);
define CONS = lambda a.lambda b.lambda c.(IF c a b);
define CAR = lambda c.(c True);
define CDR = lambda c.(c False);
define lazy FIX = lambda M.((lambda x.(M (x x))) (lambda y.(M (y y))));
define Zero = False;
define One = lambda f.lambda x.(f x);
define PLUS = lambda m.lambda n.lambda f.lambda x.(m f (n f x));
define TIMES = lambda m.lambda n.lambda f.lambda x.(m (n f) x);
//define lazy INFINITY = (lambda x.(x x)) (lambda x.(x x));
define NULL = False;
define M = (CONS 2 (CONS 3 (CONS 5 (CONS 7 NULL))));
(K 1); // lambda y.1
(K 1 2); // 1
(K I); // lambda x.lambda y.y
(K I 2); // lambda y.y
(K I 2 3); // 3
//weak (S K I); // weak head normal form
(S K I); // full normal form
(S K I I); // lambda x.x
(S K I 0); // 0
// booleans and if-else
(IF (AND (NOT False) True) 1 2); // 1
// linked lists:
(CAR (CDR (CDR M))); // 5
// arithmetic
(PLUS One One); // 2 in church numeral
(TIMES (PLUS One One) Zero 1 0); // 0: 2*0=0!
// static scoping:
let x = 1 in
(let f = lambda y.x in
(let x = 2 in (f 0))); // 1, since lambda calc implies static scoping.
// if 2 was printed, then it's dynamically scoped
// and something went horribly wrong.