The integers (and other constants) can be defined in the λ calculus; it is not necessary to provide them as "built in". However this "implementation" of integers is not efficient and so they invariably are built into programming languages based on the λ calculus.

Here is a λ calculus definition of non-negative integers and some operators on them:-

integers

let rec
  ZERO = lambda s. lambda z. z,
  ONE  = lambda s. lambda z. s(z),
  TWO  = lambda s. lambda z. s(s(z)),
  THREE= lambda s. lambda z. s(s(s(z))),{etc.}

  PLUS = lambda x. lambda y.
    lambda s. lambda z. x s (y s z),
  {traditional defn of + }

  SUCC = lambda x. lambda s. lambda z. s(x s z),
  {successor function}

  PLUSb = lambda x. x SUCC,
  {a nicer alternative defn of +, PLUS}

  TIMES = lambda x. lambda y. x (PLUS y) ZERO,

  PRED = lambda n. lambda s. lambda z.
    {NB. PRED ZERO = ZERO}
    let s2 = lambda n. lambda f. f(n s),
        z2 = lambda f. z
    in n s2 z2 (lambda x.x),

  ISZERO = lambda n. n (lambda x. false) true,

  LE =  lambda x. lambda y. ISZERO (MONUS x y),
  { ? x <= y ? }

  MONUS = lambda a. lambda b. b PRED a,
  {NB. assumes a >= b >= 0}

  DIVMOD = lambda x. lambda y.
    let rec dm = lambda q. lambda x.
      if LE y x then {y <= x}
        dm (SUCC q) (MONUS x y)
      else pair q x
    in dm ZERO x,

  DIV = lambda x. lambda y. DIVMOD x y fst,
  MOD = lambda x. lambda y. DIVMOD x y snd,

  pair = lambda fst. lambda snd. lambda sel. sel fst snd,
  fst  = lambda x. lambda y. x, {see}
  snd  = lambda x. lambda y. y, {Bool}

  PRINT = lambda n. n (lambda m. 'I'::m) '.'

in let rec {e.g.}
  four  = MONUS (TIMES THREE TWO) (PLUS ONE ONE),
  eight = PLUSb four four
in
PRINT (DIV eight THREE)

{ Define (non -ve) Int From Scratch. }

e.g.,

PLUS ONE TWO

= (λ x. λ y. λ s. λ z. x s (y s z))    --PLUS
   (λ s. λ z. s(z))                    --ONE
    (λ s. λ z. s(s(z)))                --TWO

= (λ y. λ s. λ z.
     ((λ s'. λ z'. s'(z')) s (y s z)))
    (λ s. λ z. s(s(z)))

= (λ y. λ s. λ z. (s(y s z)))
    (λ s. λ z. s(s(z)))

= λ s. λ z.
   s( (λ s". λ z". s"(s"(z"))) s z)

= λ s. λ z. s(s(s(z)))

= THREE

Here, integers are PRINTed in unary notation. (Well, you try defining a binary or decimal print routine this way – exercise!-)

 

let rec ZERO = lambda s. lambda z. z, ONE = lambda s. lambda z. s(z), TWO = lambda s. lambda z. s(s(z)), THREE= lambda s. lambda z. s(s(s(z))),{etc.} PLUS = lambda x. lambda y. lambda s. lambda z. x s (y s z), {traditional defn of + } SUCC = lambda x. lambda s. lambda z. s(x s z), {successor function} PLUSb = lambda x. x SUCC, {a nicer alternative defn of +, PLUS} TIMES = lambda x. lambda y. x (PLUS y) ZERO, PRED = lambda n. lambda s. lambda z. {NB. PRED ZERO = ZERO} let s2 = lambda n. lambda f. f(n s), z2 = lambda f. z in n s2 z2 (lambda x.x), ISZERO = lambda n. n (lambda x. false) true, LE = lambda x. lambda y. ISZERO (MONUS x y), { ? x <= y ? } MONUS = lambda a. lambda b. b PRED a, {NB. assumes a >= b >= 0} DIVMOD = lambda x. lambda y. let rec dm = lambda q. lambda x. if LE y x then {y <= x} dm (SUCC q) (MONUS x y) else pair q x in dm ZERO x, DIV = lambda x. lambda y. DIVMOD x y fst, MOD = lambda x. lambda y. DIVMOD x y snd, pair = lambda fst. lambda snd. lambda sel. sel fst snd, fst = lambda x. lambda y. x, {see} snd = lambda x. lambda y. y, {Bool} PRINT = lambda n. n (lambda m. 'I'::m) '.' in let rec {e.g.} four = MONUS (TIMES THREE TWO) (PLUS ONE ONE), eight = PLUSb four four in PRINT (DIV eight THREE) {<B> Define (non -ve) Int From Scratch. </B>}

output area

 

Also see [Boolean] and [Lists].

Thanks to Joel Reicher for the TIMES, LE and DIVMOD examples.