A Gentle Introduction to Lambda Calculus - Part 1: Syntax
You will also find, at the end of each post, a list of recommended resources to learn more about it in case you’re interested.
I’ve also recently written about my favorite combinator: the Y-Combinator and I highly recommend you to read that too if you end up liking this post.
Without further ado, let’s talk about what matters to us here: Lambda Calculus.
What is Lambda Calculus?
Any of the computer programs we have ever written and any of the ones that are still unwritten can be expressed using either Lambda Calculus or a Turing Machine.
As I’ve mentioned in the introduction to this post, I could write an entire blog post contextualizing this, but now that you know what Lambda Calculus is and what it does, let’s get to the practical stuff.
Lambda Calculus’ Syntax
Everything in Lambda Calculus is an expression, which means that everything must evaluate to a value.
There are, however, four different forms of expressions (which I’ll call
E can be either:
λID. E- Abstraction.
E E- Application
Identifiers are simply that: identifiers. They identify certain values by giving them a “name”, just like our modern programming languages do.
const x = 10 x // Identifier equivalent
Abstractions are perhaps the most iconic kind of lambda expression, they define what we call functions or, more adequately, lambdas: which are just anonymous functions. The
ID in the beginning of that abstraction is called the metavariable. The metavaraible is the variable that is going to be used in the function’s body (which in this case is
E), for example:
(x) => x * x // Abstraction equivalent
Applications denote function invocation. If you have a function
A you can say you’re calling it with
B by writing
const a = (x) => x * x const b = 10 a(b) // Application equivalent
Grouping exists for the sake of disambiguation. We use these parentheses around the expressions we want to group to make it clear which ones of them we want to apply to each other. If this doesn’t make much sense now don’t worry, it will in a few paragraphs.
Bound and Free Variables
In lambda calculus, it is very important to understand the concept of bound and free variables, so that we can explore combinators later.
(I’ll now shamefully copy the explanation I’ve used for bound and free variables from my Y-Combinator post, because good programmers know what to write, great ones know what to reuse)
Free variables are variables defined outside of the function’s scope. They’re the opposite of bound variables, which are variables that only exist inside of a function’s scope.
const num = 13; const sumPlusThirteen = (a, b) => a + b + num
In the snippet above, our function
sumPlusThirteen uses the variables
num. The variables
b are bound variables because they are bound to the function’s parameters: when we refer to their names we are referring to values that were passed to the
sumPlusThirteen function. However, the variable
num refers to a value outside of the function’s scope, which means it is a free variable.
Let’s look at some more examples:
x => x-
xis a bound variable, because it’s bound to the function’s parameters
x => x(y)-
xis a bound variable because it’s bound to the function’s parameters and
yis a free variable because it refers to a value outside of the function’s scope
x => y(z)-
zare both free variables because they refer to values outside of the function’s context
(x, y) => x(y)- Both
yare bound variables because they are bound to the function’s parameters
Now, the same examples above, but in using Lambda Calculus’ syntax:
xis a bound variable
λx. x y-
xis a bound variable and
yis a free variable
λx. y z-
zare both free variables
λx. λy. x(y)- Both
yare bound variables
In Lambda Calculus, each abstraction cannot take more than one argument, which means that we have to do currying in order to be able to work with multiple variables in the body of a function.
Currying consists in translating a single function with multiple arguments into series of nested functions which take one argument each.
const sum = (a, b) => a * b sum(2, 3) // 6 // Or, more adequately: ((a, b) => a * b)(2, 3) // 6
However, you cannot do this in Lambda Calculus. In order to have these two variables available in an expression we would have to nest one lambda inside the other so that both
b are available to the innermost function’s body:
const product = (a) => (b) => a * b; product(2)(3) // 6 // Or, more adequately: ((a) => (b) => a * b)(2)(3) // 6
In the example above, when we call
2 what we’re doing is returning another function which is
(b) => a * b in which
a is already bound to the
a metavariable in the outermost function.
Similarly, if you wanted to have more arguments you could just keep wrapping your lambdas in other lambdas:
const product = (a) => (b) => (c) => a * b * c; product(2)(3)(4) // 24 // Or, more adequately: ((a) => (b) => (c) => a * b * c)(2)(3)(4) // 24
Now, in a bit more conventional lambda calculus syntax:
λa. λb. a * b
More importantly than knowing how Lambda Calculus works, is being able to read it correctly, otherwise, all you’ve learned until now would have little to no use.
How would you read the lambda expression
x y z for example? Should it be interpreted as
Applications are left associative, which means that the terms are grouped from left to right. In the previous example, you would then disambiguate
x y z as
(x y) z. This means you could disambiguate
a b c d as
((a b) c) d.
λx. x y mean
(λx. x)(y) or
Abstractions extend as to the far right as possible. For
λx. x y a plausible disambiguation could be
λx. x(y), meaning that the outermost lambda expression applies
y to the passed
λx. λy. x we could write
λx. (λy. x): which means that the outermost lambda expression evaluates to
References & Resources for the Curious
- Gödel’s Incompleteness Theorem - Numberphile
- Computerphile has this awesome series of 3 videos about the history of undecidability, which has a lot to do with the theory of computation. I highly encourage you to watch all of them: Part 1, Part 2, and Part 3
- First lecture by Adam Doupé about Lambda Calculues at Arizona State University
- Understanding Computation - Tom Stuart
- The Impact of Lambda Calculus in Logic and Computer Science - Henk Barendregt
- Introduction to Lambda Calculus - Henk Barendregt & Erik Barendsen
- Computability and Incomputability - Robert Soare
- Computability and Recursion - Robert Soare
- The History and Concept of Computability - Robert Soare
In the next few posts of this series, you will also notice that I simplified a few things in this first post to make it easier to follow, such as using the
* operators inside lambdas or even numbers, which is something I’ll talk about in the future.
For now, focus on understanding what lambda calculus itself is and its syntax constructs.
Reviewed by: Alex Dawkins 🇬🇧