The Surface of Lambda Calculus

Last updated: July 16, 2018

Image by Lapse via wallhaven

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?

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:


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.


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.


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:


Last example before we discuss further:


We take c then substitute it for the first bound variable a:


We then take d then substitute it for b which will result to:



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:


To get to 1, we simply append a duplicate of the first bound variable which is a immediately after the . which will result to:


The advanced functions


We'll start first with the Successor function which is defined as:


What this function does is it finds the result after adding one to a whole number. Let's try it with the number two:


Substitute the first bound variable a with the function for number two:


We now apply the number two function to the bc in the function body:


The result is now the function for number three.


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:


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.


We now do the magic of expansion then reduction:

= 3


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:


To multiply two and two, we proceed like this:

= (λ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
= s

Fsz = (λab.b)sz
= 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

= (λbc.c)(λde.d)(λfg.g)
= T


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:


To serve as the base for the final form of the predecessor function, we'll use the zeroth pair:


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:


Let's apply it to our zeroth pair:


We can now build the main predecessor function:


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:

(λfg.g) ((λrm.r(m))(λrm.m))
= 0

With the predecessor function being built, the subtraction function can now be formulated:


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:

= 1