The Surface of Lambda Calculus
In this short guide, I will discuss how I understood Lambda Calculus through the online journal entry of ebzzry titled A Lambda Calculus Primer.
Table of Contents
- What is lambda calculus?
- Where do we start?
- How to apply lambda calculus functions
- The advanced functions
What is lambda calculus?
Lambda Calculus, simply, is a standard method of expressing computations.
Where do we start?
Before we proceed to the meat of the topic, we need to define terms that we'll use throughout this documentation. A function is a piece of code that when executed or called, performs a task. This is what a basic function in lambda calculus looks like:
(λa.a)
In lambda calculus, this is what they call an identity function and I'll discuss later a bit of what it does and how it works. Let's dissect a bit what is contained within a lambda calculus function. The λ, which is a Greek letter meaning lambda, indicates that whatever is after it is a function. The letter or symbol after the λ preceding the . is the parameter or the name of the function, and the succeeding letter or symbol after the . is the body of the function. Symbols that reside between the λ and . are called bound and I'll show you in the next section how these bound things behave.
How to apply lambda calculus functions
We will start with something simple and we'll use the identity function to demonstrate how function applications work in lambda calculus.
(λa.a)b
The output of the function application above is b. Why, you ask? Let's break it down. The b in the snippet above is what the identity function is applied to. In lambda calculus, what we do is we substitute the b for the first bound variable after the λ symbol which is a. After the substitution, which will consume the a, we also substitute b for every occurrence of the symbol a that appears in the function body which will result in the output b. Let's take a small step forward to attempt to possibly clarify this application.
(λba.b)r
In the snippet above, we will apply the function (λba.b) to r and I won't tell you the output yet so let's walk through the process. The symbols before the . and after the λ are bound but our higher concern is the symbol immediately succeeding the λ symbol which is b because that is what we will be substituting r for. We now substitute r for the bound variable b, therefore consuming it, then we also substitute r for every occurrence of the bound variable we substituted inside the function body, which will result to:
(λa.r)
Last example before we discuss further:
(λab.a(b))cd
We take c then substitute it for the first bound variable a:
(λb.c(b))d
We then take d then substitute it for b which will result to:
cd
Numbers
Before we move to the more complicated functions, let's first establish how numbers are expressed as functions in lambda calculus. As a basis, the number zero is expressed as:
(λab.b)
To get to 1, we simply append a duplicate of the first bound variable which is a immediately after the . which will result to:
(λab.ab)
The advanced functions
Successor
We'll start first with the Successor function which is defined as:
(λabc.b(abc))
What this function does is it finds the result after adding one to a whole number. Let's try it with the number two:
(λabc.b(abc))2
(λabc.b(abc))(λde.d(d(e)))
Substitute the first bound variable a with the function for number two:
(λbc.b((λde.d(d(e)))bc))
We now apply the number two function to the bc in the function body:
(λbc.b((λe.b(b(e)))c))
(λbc.b(b(b(c))))
The result is now the function for number three.
Addition
To add in lambda calculus, you just need to modify a little your usage of the successor function. With addition, you position the successor function in between the whole numbers you're trying to add or simply called as an infix, like this:
1S2
You can further reduce it in a way through spelling out the equivalent functional notation which is equivalent to one S (single S) and a 2.
S2
We now do the magic of expansion then reduction:
S2
(λabc.b(abc))2
(λbc.b(2bc))
(λbc.b((λde.d(d(e)))bc))
(λbc.b((λe.b(b(e)))c))
(λbc.b(b(b(c))))
= 3
Multiplication
To multiply, instead of putting the function in between the numbers or as an infix, we'll use a prefix syntax. The multiplication function is defined as:
(λabc.a(bc))
To multiply two and two, we proceed like this:
(λabc.a(bc))22
(λbc.2(bc))2
(λc.2(2c))
(λc.(λde.d(d(e)))(2c))
(λc.(λde.d(d(e)))((λfg.f(f(g)))c))
(λc.(λde.d(d(e)))(λg.c(c(g))))
(λc.(λe.(λg.c(c(g)))((λg.c(c(g)))e)))
(λc.(λe.(λg.c(c(g)))(c(c(e)))))
(λc.(λe.(c(c(c(c(e)))))))
= (λce.c(c(c(c(e)))))
= 4
Boolean functions
The true and false functions in lambda calculus are pretty simple:
True(T) = (λab.a)
False(F) = (λab.b)
What the functions above do is when given a pair to be applied to like ab or cd, the true function will result in the first of the pair hence a while the false function will give the second, b. Let's experiment:
Tsz = (λab.a)sz
(λb.s)z
= s
Fsz = (λab.b)sz
(λb.b)z
= z
And or Not?
For these three logical operators, we'll import from the boolean functions:
And(∧) = λab.ab(λcd.d) = λab.ab(F)
Or(∨) = λab.a(λcd.c)b = λab.a(T)b
Not(¬) = λa.a(λbc.c)(λde.d) = λa.a(F)(T)
Let's try the Not function on F
¬F
λa.a(λbc.c)(λde.d)F
λa.a(λbc.c)(λde.d)(λfg.g)
= (λbc.c)(λde.d)(λfg.g)
= FFT
(λbc.c)(λfg.g)(λde.d)
(λc.c)(λde.d)
(λde.d)
= T
Predecessor
The predecessor function is the function reverse of the successor function because instead of adding 1, you deduct 1 from the whole number you are applying it to.
Before we proceed to defining the actual predecessor function, we have to define first, in a way, the prerequisite information needed to have a better understanding of how the predecessor function was formed.
First, you'll be needing a pair which looks like (b, a), but in this pair, the first element is one notch higher than the second element, meaning, the first element b is the successor of the second element a which also means that a is the predecessor of b. With that being said, to determine the predecessor of a, you create a pair like the one previously mentioned, select the second element (which is done by the false boolean function), then it will look like (a, ?).
A pair in lambda calculus function form looks like:
(λa.a(bc))
To serve as the base for the final form of the predecessor function, we'll use the zeroth pair:
(λc.c(00))
One last thing before we proceed to the final form of the predecessor function, we'll define a separate function whose task is to take a pair, then output a new pair, wherein in this new pair, the first element is the successor of the second element:
Z
(λab.b(S(aT))(aT))
Let's apply it to our zeroth pair:
Z(λc.c(00))
(λab.b(S(aT))(aT))(λc.c(00))
(λab.b(S(aT))(aT))(λc.c((λhi.i)(λhi.i)))
(λb.b(S((λc.c((λhi.i)(λhi.i)))T))((λc.c((λhi.i)(λhi.i)))T))
(λb.b(S(λhi.i))(λhi.i))
(λb.b(λhi.h(i)(λhi.i)))
(λb.b10)
We can now build the main predecessor function:
P
(λa.aZ(λc.c(00)))F
You'll notice that the main difference is that there's a false boolean function appended at the end and that will select the second element from the resulting pair which will be the predecessor element we're looking for. Let's test it on the number one:
P1
((λa.aZ(λc.c(00)))F)1
(1Z(λc.c(00)))F
(λab.abZ(λc.c(00)))F
(λab.ab(λab.b((S(aT))(aT)))(λc.c(λrm.m)(λrm.m)))(λfg.g)
(λb.(λab.b((S(aT))(aT)))(λc.c(λrm.m)(λrm.m))b)(λfg.g)
((λab.b((S(aT))(aT)))(λc.c(λrm.m)(λrm.m)))(λfg.g)
(λb.b((S((λc.c(λrm.m)(λrm.m))T))((λc.c(λrm.m)(λrm.m))T)))(λfg.g)
(λb.b((S(λrm.m))(λrm.m)))(λfg.g)
(λb.b((λrm.r(m))(λrm.m)))(λfg.g)
(λfg.g) ((λrm.r(m))(λrm.m))
(λg.g)(λrm.m)
(λrm.m)
= 0
With the predecessor function being built, the subtraction function can now be formulated:
R
(λab.bPa)
The function above means that the larger element b comes before the smaller element a and in between them is the predecessor function. Let's try it with two and one:
R21
(λab.bPa)(λcd.c(c(d)))(λcd.c(d))
(λb.bP(λcd.c(c(d))))(λcd.c(d))
(λcd.c(d))(P(λcd.c(c(d))))
(λcd.c(d))(λcd.c(d))
(λd.(λcd.c(d))d)
(λcd.c(d))
= 1
