Booleans

true = (lambda x (lambda y x))
false = (lambda x (lambda y y))

not = (lambda p (lambda a (lambda b ((p b) a))))
and = (lambda p (lambda q ((p q) p)))
or = (lambda p (lambda q ((p p) q)))

Church Numerals

zero = (lambda f (lambda x x))
one = (lambda f (lambda x (f x)))
two = (lambda f (lambda x (f (f x))))
three = (lambda f (lambda x (f (f (f x)))))
four = (lambda f (lambda x (f (f (f (f x))))))
five = (lambda f (lambda x (f (f (f (f (f x)))))))
six = (lambda f (lambda x (f (f (f (f (f (f x))))))))
seven = (lambda f (lambda x (f (f (f (f (f (f (f x)))))))))
eight = (lambda f (lambda x (f (f (f (f (f (f (f (f x))))))))))
nine = (lambda f (lambda x (f (f (f (f (f (f (f (f (f x)))))))))))
ten = (lambda f (lambda x (f (f (f (f (f (f (f (f (f (f x))))))))))))

succ = (lambda n (lambda f (lambda x (f ((n f) x)))))
plus = (lambda m (lambda n (lambda f (lambda x ((m f) ((n f) x))))))
mult = (lambda m (lambda n (lambda f (lambda x ((m (n f)) x)))))
pred = (lambda n (lambda f (lambda x (((n (lambda g (lambda h (h (g f))))) (lambda u x)) (lambda u u)))))
sub = (lambda m (lambda n ((n (lambda n (lambda f (lambda x (((n (lambda g (lambda h (h (g f))))) (lambda u x)) (lambda u u)))))) m)))
pow = (lambda b (lambda e (e b)))

ifthenelse = (lambda p (lambda a (lambda b ((p a) b))))
isZero = (lambda n ((n (lambda x (lambda x (lambda y y)))) (lambda x (lambda y x)))) 
leq = (lambda m (lambda n ((lambda n ((n (lambda x (lambda x (lambda y y)))) (lambda x (lambda y x)))) (((lambda m (lambda n ((n (lambda n (lambda f (lambda x (((n (lambda g (lambda h (h (g f))))) (lambda u x)) (lambda u u)))))) m))) m) n))))

Data Structures (pairs, lists)

pair = (lambda x (lambda y (lambda z ((z x) y))))
first = (lambda p (p (lambda x (lambda y x))))
second = (lambda p (p (lambda x (lambda y y))))
cons = (lambda x (lambda y (lambda z ((z x) y))))
head = (lambda p (p (lambda x (lambda y x))))
tail = (lambda p (p (lambda x (lambda y y))))
nil = (lambda x (lambda x (lambda y x)))
isempty = (lambda l (l (lambda h (lambda t (lambda x (lambda y y))))))

Y-Combinator

A lambda-term that allows for recursion to be implemented in Lambda Calculus.

ycomb = (lambda f ( (lambda x (f (x x))) (lambda x (f (x x))) ))

Factorial function in Lambda Calculus

fact = (lambda f (lambda x (((ifthenelse (isZero x)) one) ((mult x) (f (pred x))))))

f1 = ((ycomb fact) one)
f2 = ((ycomb fact) two)
f3 = ((ycomb fact) three)
f4 = ((ycomb fact) four)
f5 = ((ycomb fact) five)

Max and Min of two numbers

max = (lambda x (lambda y (((((ifthenelse leq) x) y) y) x) ))
min = (lambda x (lambda y (((((ifthenelse leq) x) y) x) y) ))

Some functions on lists

mylist1 = ((cons one) ((cons two) ((cons three) ((cons four) ((cons five) nil)))))
mylist2 = ((cons four) ((cons ten) ((cons three) ((cons five) ((cons nine) nil)))))

slist = (lambda f (lambda x (((ifthenelse (isempty x)) zero) ((plus (head x)) (f (tail x))))))
dlist = (lambda f (lambda x (((ifthenelse (isempty x)) nil) ((cons (head x)) ((cons (head x))(f (tail x)))))))
zlist = (lambda f (lambda x (((ifthenelse (isempty x)) zero) ((plus one) (f (tail x))))))
xlist = (lambda f (lambda x (((ifthenelse (isempty x)) zero) (((ifthenelse ((leq (head x))(f (tail x)))) (f (tail x))) (head x)) )))

sumlist = ((ycomb slist) mylist1)
doublelist = ((ycomb dlist) mylist1)
sizelist = ((ycomb zlist) mylist1)
alist = ((ycomb xlist) mylist2)