// Programming with pure lambda terms, with full beta-normalization via CBN.
// Basic combinators:
define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.x z (y z);
// Booleans and if-else
define TRUE = lambda x.lambda y.x; // K A B = A
define FALSE = lambda x.lambda y.y; // (K I) A B = B
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;
// Arithmetic
define ZERO = lambda f.lambda x.x;
define ISZERO = lambda n.n (lambda z.FALSE) TRUE;
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 PRED = lambda n.lambda f.lambda x.n (lambda g.lambda h.h (g f)) (lambda u.x) (lambda u.u);
define SUBTRACT = lambda m.lambda n. n PRED m;
define LEQ = lambda m.lambda n. ISZERO (SUBTRACT m n); // <=
define EQUALS = lambda m.lambda n.AND (LEQ m n) (LEQ n m);
// Data structure (pairs, linked-list = nested pairs)
define CONS = lambda a.lambda b.lambda c.IF c a b; //pair constructor
define CAR = lambda c.c TRUE; // first element of cons pair
define CDR = lambda c.c FALSE; // second element of cons pair
define NIL = FALSE; // represents empty list
define ISNIL = lambda p.p (lambda a.lambda b.lambda z.FALSE) TRUE;
// Recursion (loops) and divergence.
define lazy INFINITY = (lambda x.(x x)) (lambda x.(x x));
define lazy FIX = lambda m.(lambda x.m (x x)) (lambda y.m (y y));
// A sample linked list
define TWO = PLUS ONE ONE;
define THREE = PLUS TWO ONE;
define FIVE = PLUS TWO THREE;
define P = (CONS TWO (CONS THREE (CONS FIVE NIL)));