Lambda-terms for testing my solutions to Exercises 1. Paste them into the evaluator at https://crypto.stanford.edu/~blynn/lambda/ and hit [Run].

Lambda Calculus Exercises 1.txt

0 = \f.\x.x
1 = \f.\x.f x
2 = \f.\x.f (f x)
3 = \f.\x.f (f (f x))
4 = \f.\x.f (f (f (f x)))
5 = \f.\x.f (f (f (f (f x))))

true  = \x.\y.x
false = \x.\y.y
if    = \p.\x.\y.p x y

pair = \x.\y.\z.z x y
fst  = \p.p true
snd  = \p.p false

isNil = \l.l (\h.\t.\x.false) true
head = fst
tail = snd

succ  = \n.\f.\x.f (n f x)
predStep = \p.pair (snd p) (succ (snd p))
pred  = \n.fst (n predStep (pair 0 0))
pred1Step = \p.pair (if (snd p) 0 (succ (fst p))) false
pred1 = \n.fst (n pred1Step (pair 0 true))
plus  = \n.n succ
minus = \n.\m.m pred n
mult  = \n.\m.n (plus m) 0
factStep = \p.pair (succ (fst p)) (mult (succ (fst p)) (snd p))
fact = \n.snd (n factStep (pair 0 1))

lengthP  = \f.\l.if (isNil l) 0 (succ (f f (tail l)))
length   = (\f.f f) lengthP
sumListP = \f.\l.if (isNil l) 0 (plus (head l) (f f (tail l)))
sumList  = (\f.f f) sumListP

rlist1 = pair 5 (pair 0 (pair 1 (pair 3 false)))
length  rlist1
sumList rlist1
 
accumI   = \l.l (\n.\m.plus n (mult 2 m)) 0
ilist1 = \f.\x.f 1 (f 1 (f 0 (f 1 x)))
accumI   ilist1

lengthI  = \l.l (\n.succ) 0
sumListI = \l.l plus      0
ilist2 = \f.\x.f 3 (f 1 (f 0 (f 5 x)))
lengthI  ilist2
sumListI ilist2

pred  4
pred1 4
minus 5 3
minus 3 5
fact  3