λ

id = λx. x
const = λx y. x
fix = (λx y. y (x x y)) λx y. y (x x y)

arb = (λx. x x) λx. x x

true = const
false = const id
if = id

zero = const
suc = λn x y. y n
caseNat = λx y n. n x y
isZero = caseNat true (const false)
pred = caseNat arb id
eqNat = fix λeqNat x y.
         if (isZero x)
            (if (isZero y) true false)
            (if (isZero y) false (eqNat (pred x) (pred y)))

nil = const
cons = λa d x y. y a d
caseList = λx y l. l x y
null = caseList true (λa d. false)
car = caseList arb const
cdr = caseList arb (const id)

emptyEnv = nil
extendEnv = λe n t. cons (cons n t) e
lookupEnv = fix λlookupEnv z e n.
              if (null e)
                z
                (if (eqNat n (car (car e)))
                  (cdr (car e))
                  (lookupEnv z (cdr e) n))

var = λn x y z. x n
abs = λn a x y z. y n a
app = λa b x y z. z a b
caseTerm = λx y z t. t x y z

eval = fix λeval t.
             caseTerm
               (lookupEnv arb)
               (λv b e x. eval b (extendEnv e v x))
               (λx y e. eval x e (eval y e))