Lambdas

lambda

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)

succ := λn.λf.λx.f (n f x)
+ := λa.λb.a succ b
* := λa.λb.a (b succ) 0

pair := λa.λb.λf.f a b
fst := λc.c (λa.λb.a)
snd := λc.c (λa.λb.b)

zeroes := pair 0 0
foo := λp.pair (snd p) (succ (snd p))
onepred := λn.fst (n foo zeroes)

pz := λ_.0
pf := λg.λh.h (g succ)
id := λx.x
anotherpred := λn.n pf pz id

pred := λn.λf.λx.n (λg.λh.h (g f)) (λ_.x) id

- := λa.λb.b pred a

true := λx.λy.x
false := λx.λy.y
if := λp.λc.λa.p c a
and := λa.λb.if a b false
not := λp.λa.λb.p b a

0? := λn.n (λ_.false) true
<= := λa.λb.(0? (- a b))
= := λa.λb.and (<= a b) (<= b a)

nil := λc.λn.n
nil? := λl.l (λ_.λ_.false) true
cons := λh.λt.λc.λn.c h (t c n)
hd := λl.l (λh.λt.h) false
append := λa.λb.a cons b

nils := (cons nil nil)
bar := λh.λp.pair (snd p) (cons h (snd p))
tl := λl.fst (l bar nils)

y-comb := (λf.(λx.f (x x)) (λx.f (x x)))
fib* := λf.λn.if (<= n 1) n (+ (f (pred n)) (f (pred (pred n))))
fib := y-comb fib*

evenodd* := λf.pair (λn.if (0? n) true ((snd f) (pred n))) (λn.if (0? n) false ((fst f) (pred n)))
evenodd := y-comb evenodd*
even? := fst evenodd
odd? := snd evenodd