λ 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),
  {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!-)
 



 
Also see [Boolean] and [Lists].
Thanks to Joel Reicher for the TIMES, LE and DIVMOD examples.
www:


© L. Allison   http://www.allisons.org/ll/   (or as otherwise indicated),
Created with "vi (Linux or Solaris)",  charset=iso-8859-1,  fetched Thursday, 21-Sep-2017 01:10:52 EDT.

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