## λ calculus Integers

 LA home Computing FP  λ-calc.   Intro   Syntax   Examples    Ints    Bools    Lists(1)    arithmetic    Y (lazy)    Y (strict)    Lists(2)    Trees    Primes(1)    Fibonacci(1)    Unique    Hamming#s    Composites    Fibonacci(2)    Thue seqs.    Edit-dist.    Ints

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

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

Also see [Boolean] and [Lists].
Thanks to Joel Reicher for the TIMES, LE and DIVMOD examples.
www:
 The C++ Cookbook mastering the language

 © L. Allison   http://www.allisons.org/ll/   (or as otherwise indicated), Created with "vi (Linux or Solaris)",  charset=iso-8859-1,  fetched Thursday, 19-Apr-2018 05:52:05 EDT.

 free: Linux, Ubuntu operating-sys, OpenOffice office-suite, The GIMP ~photoshop, Firefox web-browser, FlashBlock flash on/off.