
This post is part of the Lambda Calculus series.
Algorithms have been an essential part of mathematics since it’s earliest days. Arithmetic algorithms such as long multiplication and long division are likely to be familiar to you, and some of these have been around for millennia, as early as 2500 BC. In the 3rd century BC, the algorithm called the ‘sieve of Eratosthenes’ was developed by the Greeks to find prime numbers. With the development of computers, which are essentially just machines that can carry out algorithms, the world has been transformed.
Despite their presence throughout human history, algorithms themselves were never really studied until recently. However, with the development of computers and the increasing formalisation of maths, a rigorous discussion of algorithms became inevitable. What’s more, as with many new developments, several different mathematicians attempted this formalisation at more or less the same time. The two approaches that are most widely used are Turing Machines (developed, but not named, by Turing) and the Lambda Calculus (developed and named by Church). In this series, we will focus on the Lambda Calculus—while it appears much more detached from modern computer hardware than Turing Machines, it is, in my opinion, far more elegant and beautiful.
The Foundation of Computation
One important question that should be answered by a theory of algorithms and computation is what the fundamental operations are. In other words, what is the simplest language you need to be able to describe any algorithm. This may seem like a purely academic question—it is likely to be beyond inconvenient to actually describe an algorithm using these fundamental operations—but it actually has important practical implications. When designing computer hardware and programming languages, you should, at a bare minimum, make sure that it can handle these fundamental operations. If you fail to do so, there will be some algorithms that it will be unable to perform!
In the ‘What is Maths’ series, we used addition by 1 as the fundamental operation in Number Theory. When discussing algorithms, however, there isn’t such a natural feeling fundamental operation—Church and Turing took two totally different approaches.
In Turing Machines, the algorithm and the data it’s working with are kept separately. The data is a list of 0s and 1s and the algorithm is always focused on a single item in that list. At each step, it may update the currently focused item, shift its focus left or right, and decide the next step to perform based on whether the currently focused item is a 0 or a 1.
In the Lambda Calculus, there is no fundamental distinction between algorithm and data. Any data can be interpreted as an algorithm and any algorithm can be treated as data, although it may not always make sense to do so. The fundamental operation of Lambda Calculus is substitution: locating a symbol and replacing it with some other sequence of symbols.
Despite the radical differences between these two approaches, they were proven to be equivalent in the seminal Church-Turing thesis. The idea behind this proof is remarkably simple: provide an algorithm described in the language of Lambda Calculus that can simulate any Turing Machine, and an algorithm described in the language of Turing Machines that can simulate the Lambda Calculus. The details of this proof, however, are anything but simple. In addition, it was argued in this thesis that the Lambda Calculus and Turing Machines are a good definition for computation. While definitions cannot be proven to be true or untrue, this proposal has been, as far as I’m aware, universally accepted. Furthermore, the argument for this definition has only been strengthened in the years since—every subsequent attempt at defining computation is either equivalent to the two above or less powerful.
The Terms in Lambda Calculus
Everything in the Lambda Calculus is made up of ‘terms’ and, as mentioned above, these are used to represent both algorithms and data. There are three rules by which we can construct terms and, furthermore, if something cannot be constructed by these rules, it is not a term of Lambda Calculus.
The first rule is that ‘variables’ are terms. We will represent variables with lower case letter from the English alphabet; for example
The second rule is that of application: if
The third and final rule is that of lambda abstraction, and the namesake of the Lambda Calculus itself. It states that if
Before we move on, I would like to make a subtle point about these shorthands clear: something like
Substitution
The heart of computation in the Lambda Calculus is substitution. There are two kinds of substitution we can perform, which are called
The simpler substitution rule is
For cases such as the above where several steps are needed to transform one term into another, we introduce the
Instead of applying
The other substitution rule,
When using
Finally, we introduce the
I imagine that, at this point, this may all seem like pointless symbol shuffling. However, in the next part, we’ll explore how we can represent data in this system and start to develop useful functions.