Church's Lambda Calculus

Combinators and Lambda Models for Numbers and Arithmetic

The lower part of this Calculator will evaluate (reduce) Lambda expressions or find an combinator expression which is equivalent using only S K and I combinators. Names of models or combinators can be defined in the top part.

Combinators and Models
- Some predefined Combinators and Models are supplied in the Calculator.
- A combinator is always a single uppercase letter.
- Models are lowercase words of one or more letters.
Numbers
- are defined by a JavaScript function that generates a string for the lambda expression for a positive integer including zero.
- As with other models to use a model of a number, enclose the integer in square brackets, such as [5].
- A default example of a number-defining JavaScript function is supplied and, using it, [5] means "\f.\x.f(f(f(f(fx))))" applying a function (f) 5 times to an argument (x).
- Remember to alter the models for iszero and other number-processing models to match your number-generating lambda expression.
- Use the top Expression input area to Reduce your models. For example
  [eq]([power][2][3])[8] will reduce to the model of true: \b.\c.b or some equivalent if the parameters (the bound variables) are given alternative names
Definitions
- The DEFINITIONS area is editable so that you can change definitions
- The Definitions can be restored to the defaults by using the button.
- The format of a definition is
  - the name of the model or combinator
  - followed by "="
  - then the lambda expression it stands for which may use earlier-defined model names or combinators
  - spaces are ignored
- Both models and combinators must be defined before use in other models or combinator definitions, that is,it must have been defined earlier in the list.
- Definitions cannot be recursive unless using the Y combinator or another recursive-simulation method
- To use a model in the body of another definition, enclose it in square brackets [] or else it will be interpreted as an application of single letter variables.
  Combinators are a single uppercase letter and are not enclosed in [] brackets when used in a definition.
- Three sets of Definitions are predefined and editable.
  Use the Show buttons to read them in to the Definitions area:
  - Church's Models and others useful for modelling mathematics and computing constructs
  - Standard Combinators: B,C,F,I,J,K,P,S,T,W,X
  - Turner's Combinators used to optimize Combinator expressions
  These three are automatically Defined when showing in the Definitions area.
- When the definitions are changed, use the button to reload the definitions making them usable in the Lambda Expression input box.
  The Definitions area always shows all the names that will be defined and only those are usable in Lambda expressions.

Lambda Models Calculator

Lambda Models C A L C U L A T O R

D E F I N I T I O N S

B = \f.\g.\x.f(gx)
C = \f.\x.\y.fyx
F = \f.\g.\h.\x.f(gx)(hx)
I = \x.x
J = \a.\b.\c.\d.ab(adc)
K = \x.\y.x
P = \f.\g.\x.\y.f(gx)(gy)
S = \x.\y.\z.xz(yz)
T = \x.\y.yx
W = \f.\u.fuu
X = \a.aKSK
Y = \f.ff

V = \c.\f.\g.\x.c(fx)(gx)
A = \c.\f.\g.\x.c(f(gx))
D = \c.\f.\g.\x.c(fx)g
U = \f.\p.\x.\y.(fx)y

true = \a.\b.a
false = \a.\b.b
if = \c.\t.\e.cte
not=\a.[if]a[false][true]
and = \a.\b.(\a.\t.\e.ate)aba
or = \a.\b.(\a.\t.\e.ate)aab
nand = \a.\b.[not] ([and] ab)
nor = \a.\b.[not] ([or] ab)

pair = \a.\b.\f.fab
fst = \p.p(\a.\b.a)
snd = \p.p(\a.\b.b)

nil = \l.l(\i.i)
cons = \a.\l.\f.fal
head = \l.l\h.\t.h
tail = \l.l\h.\t.t
isnull = \l.l(\x.\y.\a.\b.a)(\i.i)

iszero = \n.n(\y.[false])[true]
succ = \n.\f.\x.f(nfx)
pred = \n.[snd](n(\p.[pair]([succ]([fst]p))([fst]p))([pair][0][0]))
sum = \m.\n.\f.\x.mf(nfx)
prod = \m.\n.\f.m(nf)
power = \m.\n.nm
diff = \m.\n.n[pred]m
min = \m.\n.[diff]m([diff]mn)
max = \m.\n.[diff]([sum]mn)([min]mn)
le = \m.\n.[iszero]([diff]mn)
ge = \m.\n.[le]nm
eq = \m.\n.[and]([le]mn)([le]nm)
ne = \m.\n.[not]([eq]mn)
lt = \m.\n.[not]([ge]mn)
gt = \m.\n.[not]([le]mn)

tri = Y (\f.\n.[if]([iszero]n)[0]([sum]n(f f ([pred]n))))
mod = Y (\f.\m.\n.[if]([lt]mn)m(f f ([diff]mn)n))
  evenq = \n.[iszero]([mod]n[2])
  oddq = \n.[not]([evenq]n)
div = Y(\f.\m.\n.[if]([lt]mn)[0]([succ](f f ([diff]mn) n)))
fact= Y(\f.\n.[if]([iszero]n)[1]([prod]n(f f ([pred]n))))

ptestfrom = Y(\f.\n.\d.[if]  ([le]([prod]dd)n) ([and]  ([not] ([iszero]([mod]nd)))  (f f n ([sum][2]d)))  [true])
primeq = \n.[or]([eq]n[2])([and]([not]([iszero]([mod]n[2])))([ptestfrom]n[3]))

range = Y(\r.\s.\e.[if]([lt]es)[nil]([cons]s(rr([succ]s)e)))
map= Y (\r.\f.\l.[if]([isnull]l)l([cons](f([head]l))(rr f ([tail]l))))
select = Y (\r.\p.\l.[if]([isnull]l)[nil]((\t.[if](p([head]l))([cons]([head]l)t)t)(rrp([tail]l))))
takewhile = Y (\r.\c.\l.[if](c([head]l))([cons]([head]l)(rr c ([tail]l)))[nil])
foldl = Y (\r.\f.\a.\l.[if]([isnull]l)a(rrf(fa([head]l))([tail]l)))
foldr = Y (\r.\f.\a.\l.[if]([isnull]l)a(f([head]l)(rrfa([tail]l))))

Model for integer n:

Head:

Body(0)=
Body(n)=

Lambda expression using Definitions

R E S U L T S

The Models

Church showed that using Lambda expressions and reduction alone we could find lambda expressions that 'modelled' mathematics including arithmetic. His 'thesis' is that all of mathematics that is computable can be modelled in the Lambda Calculus. The Lambda Calculus has been shown to be equivalent to a universal Turing machine in that what one can model so can the other. This in a sense defines what we mean by 'computable' mathematics.
The models are as follows:

Math definition

Lambda model
name = definition

Arity
#args

Notes and examples

Boolean values and operations

True

[true]

\a.\b.a

Boolean values

False

[false]

\a.\b.b

Conditional expression

[if]

\c.\t.\e.cte

if(condition,thenVal,elseVal)

= thenVal, if condition is True
= elseVal, if condition is False

not

[not]

\a.[if]a[false][true]

Boolean negation

and

[and]

\a.\b.aba

Boolean conjunction

[or]

\a.\b.aab

Boolean disjunction

nand

[nand]

\a.\b.[not] (aba)

not(A and B)

nor

[nor]

\a.\b.[not] (aab)

not(A or B)

Tuples: having a fixed length

pair

[pair]

\a.\b.\f.fab

Make a tuple (a,b)

First

fst

\p.p(\a.\b.a)

Select the first (a) from a pair (a,b)

Second

snd

\p.p(\a.\b.b)

Select the second (b) from a pair (a,b)

Lists of changeable length

Nil

[nil]

\l.l(\i.i)

The empty list

Cons

[cons]

\a.\l.\f.fal

Construct a list from an element and a list

Head

[head]

\l.l\h.\t.h

Select the first item from a list

Tail

[tail]

\l.l\h.\t.t

Select the rest of a list after the first item

isNull

[isnull]

\l.l(\x.\y.\a.\b.a)(\i.i)

boolean: is a list empty?

Numerals

[0]

\f.\x.x

"Apply f N times to x"
Uses a JavaScript function to generate the model

[1]

\f.\x.fx

[2]

\f.\x.f(fx)

[3]

\f.\x.f(f(fx))

...

[n]

\f.\x.f(f...(fx)..)

Arithmetic

\n.n=0

[iszero]

\n.n(\y.[false])[true]

boolean: is a number zero?

\n.n+1

[succ]

\n.\f.\x.f(nfx)

the successor function

\n.n-1

[pred]

\n.[snd](n(\p.[pair]([succ]([fst]p))([fst]p))([pair][0][0]))

the number before;
the predecessor of 0 is 0

\a.\b.a+b

[sum]

\m.\n.\f.\x.mf(nfx)

m + n

\a.\b.a×b

[prod]

\m.\n.\f.m(nf)

m × n

\a.\p.a^p

[power]

\m.\n.nm

m ⁿ

\a.\b.|a−b|

[diff]

\m.\n.n[pred]m

the positive difference between A and B

diff(a,b)

= a−b, if a>b
= b−a, if a<b

Minimum

[min]

\m.\n.[diff]m([diff]mn)

min(a,b)

= a, if a≤b
= b, if b<a

Maximum

[max]

\m.\n.[diff]([sum]mn)([min]mn)

max(a,b)

= a, if a≥b
= b, if b>a

≤

[le]

\m.\n.[iszero]([diff]mn)

a ≤ b

≥

[ge]

\m.\n.[le]nm

a ≥ b

[eq]

\m.\n.[and]([le]mn)([le]nm)

a = b

≠

[ne]

\m.\n.[not]([eq]mn))

a ≠ b

[lt]

\m.\n.[not]([ge]mn)

a < b

[gt]

\m.\n.[not]([le]mn)

a > b

Recursive definitions

Triangular Numbers
T(n)=n(n+1)/2

[tri]

Y(\f.\n.[if]([iszero]n)[0]([sum]n(f f ([pred]n))))

T(n) = 1+2+...+n

T(n)	= 0, if n=0 = n+T(n−1), if n>0

For example T(3)=6 and [tri][3] reduces to [6]

Mod

[mod]

Y (\f.\m.\n.[if]([lt]mn)m(f f ([diff]mn)n))

a (mod b)

is even?

[evenq]

\n.[iszero]([mod]n[2])

n (mod 2)==0

is odd?

[oddq]

\n.[not]([evenq]n)

n (mod 2) ≠ 0

[div]

Y (\f.\m.\n.[if]([lt]mn)[0]([succ](f f ([diff]mn) n)))

floor(a/b) = integer part of a/b
= (a−(a mod b))/b

Factorial: n!

[fact]

Y (\f.\n.[if]([iszero]n)[1]([prod]n(f f ([pred]n))))

n! = 1×2×...×n, if n>0
0! = 1

IsPrime?

[primeq]

(f f n ([sum][2]d))) [true] \n.[or]([eq]n[2])([and]([not]([iszero]([modrec][modrec]n[2])))([ptestfrom]n[3]))
where
ptestfrom = Y (\f.\n.\d.[if] ([le]([prod]dd)n) ([and] ([not] ([iszero]([modrec][modrec]nd))) (ffn([sum]d[2]))) [true])

is n prime?
Uses an auxiliary recursive function ptestfromrec(a,b) to check odd numbers from b are not factors of a
[primeq][21] -> \a.\b.b = [false]
[primeq][19] -> \a.\b.a = [true]

List Processing

s, ... ,e

[range]

Y (\f.\s.\e.[if]([gt]es)[nil]([cons]s(ff([succ]s)e))

Makes a list of the numbers from s to e

map

[map]

Y (\m.\f.\l.[if]([isnull]l)l([cons](f([head]l))(m m f ([tail]l))))

make a new list by applying a function to each element of a list
[map] (W[sum]) ([cons][3]([cons][5][nil]))
will map the "doubling" function W[add] = \x.[sum]xx to each of the elements of list cons(3,cons(5,nil))
to give cons(6,cons(10,nil))

select

[select]

Y (\f.\p.\l.[if]([isnull]l)[nil](p([head]l)([cons]([head]l)(ffp([tail]l)))))

Select all the elements of a list L that have property P (where P applied to any element gives True for those elements to be selected)
[select][evenq]([range][3][6])
-> [cons]4([cons][6][nil])

take while

[takewhile]

Y ( \w.\p.\l.[if]([isnull]l)[nil]([cons]([head]l)(wwp([tail]l)))

Construct a new list by taking the elements of a list in turn so long as they meet a given condition
[takewhile] [evenq] ([cons][2]([cons][0]([cons][7](cons[4][nil]))))
-> [cons][2](cons[0][nil])

foldLeft

[foldl]

Y (\r.\f.\a.\l.[if]([isnull]l)a(rrf(fa([head]l))([tail]l)))

accumulate by combining the elements of a list from the left with a given function f and starting value a
for example: [foldl] f z ([cons]a([cons]b([cons]c[nil]))) → f(f(fza)b)c

foldRight

[foldr]

Y ( \f.\o.\a.\l.[if]([isnull]l)a(o([head]l)(ffoa([tail]l)) )

reduce a list by combining the elements from the right with a given function f and a given (nil) value z
for example: [foldr] f z ([cons]a([cons]b([cons]c[nil]))) → fa(fb(fcz))

Rules

... coming soon ...

Back to Dr Knott's Fibonacci Home page