## Lambda Calculus Integers

 home1 home2  Bib  Algorithms  Bioinfo  FP  Logic  MML  Prog.Lang and the  Book

FP
Lambda
Introduction
Examples
Bool
Ints
Lists
others

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

Here is a Lambda Calculus definition of non-negative integers and some operators on them:-

 ```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. } ```

For example:

 ``` PLUS ONE TWO = (λ x. λ y. λ s. λ z. x s (y s z)) (λ s. λ z. s(z)) (λ s. λ z. s(s(z))) = (λ 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 ```

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

 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. }
Also see [Boolean] and [Lists].
Thanks to Joel R. for DIVMOD, TIMES and LE, the latter nicely making the point that "you cannot do something less than 0 times."
 Coding Ockham's Razor, L. Allison, Springer A Practical Introduction to Denotational Semantics, L. Allison, CUP

 Linux  Ubuntu free op. sys. OpenOffice free office suite The GIMP ~ free photoshop Firefox web browser

λ ...
 :: list cons nil the [ ] list null predicate hd head (1st) tl tail (rest)

 © L. Allison   http://www.allisons.org/ll/   (or as otherwise indicated), Faculty of Information Technology (Clayton), Monash University, Australia 3800 (6/'05 was School of Computer Science and Software Engineering, Fac. Info. Tech., Monash University, was Department of Computer Science, Fac. Comp. & Info. Tech., '89 was Department of Computer Science, Fac. Sci., '68-'71 was Department of Information Science, Fac. Sci.) Created with "vi (Linux + Solaris)",  charset=iso-8859-1,  fetched Friday, 01-Mar-2024 16:38:28 AEDT.