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!-)