The Lambda Calculs - the origin on Functional Programming

The calculators on this page require JavaScript but you appear to have switched off JavaScript (it is disabled). The Calculators and the Contents sections and other interactions need JavaScript.
o Please go to the Preferences (Settings) for this browser and enable JavaScript, then Reload this page.

What's on this page

The

icon means there is a You Do the Maths... section of questions to start your own investigations. The

calculator icon indicates that there is a live interactive calculator in that section.

Church's Lambda Calculus

What is a basis for Mathematics?

In the early and middle parts of the 20th century much mathematical interest was focussed on the basis of mathematics: was there a finite set of axioms on which the whole of mathematics could be built just like Euclid did on which to base all his geometric constructions. Is it possible? If so, how?
Here we briefly look at 3 concepts that were posed as the basis of which all of maths could be built: sets and logic, a Turing machine and Church's Lambda Calculus. All ultimately failed in their aim but led to modern programming lanugages.

Russell's Sets and Logic

One attempt was Bertrand Russell's attempt to use sets as that basis but then he found a logical paradox about sets which include themselves which was a logical statment tht could neither be true nor false - a paradox. Think of the rule that "in a certain village everyone is clean-shaven and the town barber shaves everyone who doesn't shave themselves". At first this sounds sensible but then we ask "The barber lives int he town so who shaves the barber?" If he shaves himself then he shouldn't as the barber shaves only those who do not shave themselves. If he doesn't shave himself then, by the logical rule, he should! This showed that there are such logical paradoxes outside of logic that Russell could not model with sets.

Alan Turing's paper-tape rewriting machine

Turing also wrote about a Turing Machine that acted like a mechanical device writing and erasing squares on a paper tape. His system was shown to be equivalent to Russell's sets in that what one could describe or define, the other could too.

Church's Lambda Calculus

Alonzo Church tried to make "function" as the basis of maths in his Lambda calculus. It was also shown to describe Russell's sets and Turing's machine in that they all could define the same parts of maths that the others could. This came to define "Computable Mathematics".
Church's work is simple to understand especially for any programmer and led directly to "functions" as a practical "functional" programming language. LISP was a first attempt to o that.
Later E W DIjkstra pointed out that the bugbear of programming in the 1960s was the assignment statement which altered the value of a cariable. Also programming was littered with "go to" statements that made it impossible to follow the computational path when a program was executed. Bothe concepts he blamed for the difficulty of writing provable correct programs. This led to a renewed interest in function as a primary object in a programming language and the elimination of the assigmnet statment that changed the value of a variable.

Kurt Gödel's Theorems

G&ounl;del had shown that if there was a basis of maths that could desrive basic arithmeic then it must always have statements in it that, though true, could not be demonstrated so within that system - there were uncomputable but true statements; or else the system itself was inconsistent in that it could be used to both show the truth and falsity of a statement. This was a mathematical bomb-shell in that all attempts to put mathematics ona firm logical foundation must fail. But it left ome profound ideas that are still put to practical use today, for example modern computers can be traced back to Turing's ideas. Church's functions leads to "functional programming".
The implications of Gödel's theorems are that there will always be programs that never terminate and we can never write another program that will always detect these.

The aim of this page is to show how Lambda calculus works ( it has nothing to do with the calculus as it is used in school maths) and how it leads to the idea of pure functions as a programming language. But out functions have parameters (arguments). Another idea was to do away with even these and use pure Combinators or functions that work on other functions.

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
diffz = \m.\n.n[pred]m
min = \m.\n.[diffz]m([diffz]mn)
max = \m.\n.[diffz]([sum]mn)([min]mn)
le = \m.\n.[iszero]([diffz]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 ([diffz]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 ([diffz]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]([gt]n[2])([and]([eq]([mod]n[2])[1])([ptestfrom]n[3])))

range = Y(\r.\s.\e.[if]([lt]es)[nil]([cons]s(rr([succ]s)e)))
atindex = Y(\f.\i.\l.[if]([iszero]i)([head]l)(f f ([pred] i) ([tail]l)))
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.
Alonzo Church in his original monograph of 1941 The Calculi of Lambda-Conversion PDF used a slightly different set of models in that he did not define a model for 0 and defined "difference" between two numbers as the maximum of 1 and (a-b). We use diffz here as a model for the (a-b) or 0 if b>a. Of course, this must be defined without using a model for subtraction nor even using > which is defined later. This is to ensure we do not get circular definitions that never end. We can define two recursive functions each using the other which is explained in the section on Recursion below.

Logic

The models are as follows:

Math definition	Lambda model name = definition		Arity #args	Notes and examples
True	[true]	\a.\b.a	0	Boolean values
False	[false]	\a.\b.b	0	Boolean values
Conditional expression	[if]	\c.\t.\e.cte	3	if(condition,thenVal,elseVal) = thenVal, if condition is True = elseVal, if condition is False
not	[not]	\a.[if]a[false][true]	2	Boolean negation
and	[and]	\a.\b.aba	2	Boolean conjunction
or	[or]	\a.\b.aab	2	Boolean disjunction
nand	[nand]	\a.\b.[not] (aba)	2	not(A and B)
nor	[nor]	\a.\b.[not] (aab)	2	not(A or B)

Tuples

A tuple is a pair of values, like coordinates on a map. We need a constructor and a way of selecting the parts too.
Church also introduced triples.

Math definition	Lambda model name = definition		Arity #args	Notes and examples
pair	[pair]	\a.\b.\f.fab	2	Make a tuple (a,b)
first	fst	\p.p(\a.\b.a)	1	Select the first (a) from a pair (a,b)
second	snd	\p.p(\a.\b.b)	1	Select the second (b) from a pair (a,b)

Lists

Lists are an extension of tuples but may have a variable length. They ar constructed from an empty list (nil) and a function which adds a ne element onto the front of the list (cons) and two basic selectors to get to the head of the list and the rest of the list (its tail).

Numbers

Only positive numbers and 0 ar defined. Negative numbers can be modelled by a pair of values, the first signifying the sign of the numbers, the second its positive value, so natural numbers are more fundamental. The way Church chose to model a number N was as a function to be applied N times to an argument. Other ways are possible too.

Math definition	Lambda model name = definition		Arity #args	Notes and examples
Nil	[nil]	\l.l(\i.i)	0	The empty list
Cons	[cons]	\a.\l.\f.fal	2	Construct a list from an element and a list
Head	[head]	\l.l\h.\t.h	1	Select the first item from a list
Tail	[tail]	\l.l\h.\t.t	1	Select the rest of a list after the first item
isNull	[isnull]	\l.l(\x.\y.\a.\b.a)(\i.i)	1	boolean: is a list empty?

Math definition	Lambda model name = definition		Arity #args	Notes and examples
0	[0]	\f.\x.x	0	"Apply f N times to x" Uses a JavaScript function to generate the model
1	[1]	\f.\x.fx	0
2	[2]	\f.\x.f(fx)	0
3	[3]	\f.\x.f(f(fx))	0
...	[n]	\f.\x.f(f...(fx)..)	0

Arithmetic

Subtraction must only produce a natural number as the difference, so we use a model that produces 0 if the difference is negative.

Math definition

Lambda model
name = definition

Arity
#args

Notes and examples

\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 or 0

[diffz]

\m.\n.n[pred]m

the positive difference between A and B

diffz(a,b)

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

Comparisons

Math definition

Lambda model
name = definition

Arity
#args

Notes and examples

Minimum

[min]

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

min(a,b)

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

Maximum

[max]

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

max(a,b)

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

≤

[le]

\m.\n.[iszero]([diffz]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

is even?

[evenq]

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

n (mod 2)==0

is odd?

[oddq]

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

n (mod 2) ≠ 0

Recursive definitions

Recursion means using a function within its own definition. This would lead to an infinte call of the function so Church got round this restriction by duplication of teh recursive function and including it as an etra parameter. The Y combinator does this.

Math definition

Lambda model
name = definition

Arity
#args

Notes and examples

at rank
atindex i list = list[[i]]

[atindex]

Y(\f.\i.\l.[if]([iszero]i)([head]l)(f f ([pred] i) ([tail]l))

By indexing a list starting from index 0, this function returns the i^th element of the list, or [nil] if one does not exist.
Interestingly, [nil] is also the model for [false]

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 ([diffz]mn)n))

a (mod b)

[div]

Y (\f.\m.\n.[if]([lt]mn)[0]([succ](f f ([diffz]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]

Functions applied to lists

This method of programming was the start of what is today called Functional Programming where a function is "a first-class object" in that functions can be passed as arguments to other functions.
This makes up for the loop (do, while and repeat statements) in other programming languages.
Here are some common and useful functions to be called on lists

Math definition	Lambda model name = definition		Arity #args	Notes and examples
s, ... ,e	[range]	Y (\f.\s.\e.[if]([gt]es)[nil]([cons]s(ff([succ]s)e))	2	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))))	2	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)))))	2	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)))	2	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)))	3	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)) )	3	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