You already know lambda calculus. Here’s why.

This article aims to describe lambda calculus as simple as possible, reveal its beauty and show that they’re already know all that in some way, just in other definitions.

Why would you want to spend your time reading about such a complex thing? Because lambda calculus:

• is awesome!
• represents the foundations of any mathematical system, including programming!
• helps you to understand functional programming more deeply

Plus, it’s a good thing to know what the tools you’re using are based on, how do they work on the fundamental level.

Don’t be afraid of complex words. I’ll explain every one of them and I promise, it’s not as hard as it seems. If you’ll have any questions while reading this article, feel free to leave a comment or contact me through my website (link in my Medium profile -> “How to contact me?”). I’ll be happy to help you.

So let’s begin!

Introduction

You’ve probably heard of a scary looking mathematical thing called lambda calculus. If not, let me introduce you through an example:

Y := λz.(λx.z (x x)) (λx.z (x x))

Don’t worry, it’s just a fixed-point combinator, it’s a construct of lambda calculus and you’ve already used it as a concept many times in your life. We’ll discuss that particular thing later, it was just a syntax example. For now, let’s concentrate on the basics first.

First, let’s look at the definition: “Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.”

So, it’s a very basic yet powerful programming language that allows you to compute anything that can be computed. Yes, that means it’s Turing complete. In fact, it was invented before Turing machine by Alonzo Church, Turing’s teacher.

“Ok, that’s cool, but what does it have to do with me?”. It’s simple.

Every functional programming language is a superset of lambda calculus.

Well, except those that are built upon function-level programming. Combinatory logic languages like Backus’s FP and FL, for example. But those are rather academical and rarely used (yeah, even by FP languages standards).

So every time you write something FP-style in JavaScript or some pure FP language like Haskell, you are in fact using lambda calculus.

Now let’s see what parts is it made of and how together they are forming this beautiful elegant system.

Basics

Basic things in lambda calculus are variables, lambda terms, application and abstraction. Let’s look at each of them.

Abstraction is just a function definition. It’s indicated by the λ symbol. After this symbol you write input variables of a function, then a dot and then the output of a function where you describe what you want to get (so it’s a body of a function at the same time).

Variable in lambda calculus is the same as variable in any programming language — container for some value. Scope of a variable is defined by its closest function or parentheses. Variables in lambda calculus can be free or bound. Bound variable is a variable used in its scope after it was declared in the closest function input, otherwise it’s free.

Here “x” is bound, and “y” is free:

λx.xy

Lambda term is a basic entity in lamba calculus. Basically, it can be a variable or a function of some sort. Any variable is a valid lambda term, also every abstraction and application is a valid lambda term. Everything else is not a valid lambda-term. Lambda term can be given a name for easier reusability.

For example, an identity term (output is the same as input) is defined like this:

I := λx.x

We can use any other symbol or word instead of “I”, “I” is just a standard name for this common term. The same is true for “x”, we can call it “y” or anything else. This pretty simple and intuitive notion is called alpha conversion (alpha renaming) and it says that names of bound variables in abstraction can be changed. For variables not bound in abstraction this rule doesn’t work, meaning the “x” and “y” by themselves are not interchangeable, because they’re not equal to each other. But they are interchangeable when used as a name for input after λ symbol.

Function is a description of a process associating input to some output. Like in math and every other programming language. On top of that all functions in lambda calculus:

• are anonymous, meaning they cannot be given a name
• can only take one variable, so their arities are equal to 1
• treated as “first-class values”, meaning they can be inputs and outputs in functions

Application is a process of applying lambda term to other lambda term (variable or a function). To write an application in lambda calculus, you just need to write terms with a whitespace between them:

x y

Now, when we passed through the basics, it’s time to get to the more interesting stuff.

Diving deeper

More than 1 argument

So, previously we had established that we can only use one variable per function’s input. But how would we implement something that requires two or more variables? You’ve probably guessed it, currying! Just present the function with multiple arguments as a function with first argument that returns a function with a second argument that returns an output.

So

λxy.x

becomes

λx.λy.x

Easy-peasy.

Defining the atoms of the universe

There is nothing pre-defined in lambda-calculus except aforementioned things. Everything else needs to be added manually. Even natural numbers and TRUE/FALSE. And they are defined as functions:

0 := λf.λx.x
1 := λf.λx.f x
TRUE := λx.λy.x
FALSE := λx.λy.y

Note that FALSE definition equals to that of a 0 in lambda terms.

Substitution

Substitution is the process of replacing all free occurrences of the variable in the expression with other expression. Here’s how it looks (V is a variable):

E[V := O]

Pretty simple. It is important to meet the freshness condition, though. The variable you’re substituting with should be in free variables of the term. Otherwise, you’ll change the meaning of the function. Example of such mistake:

λx.y[y:=x] = λx.(y[y:=x]) = λx.x

“x” were an argument of our term, so by substituting “y” with it we changed function behavior. Same example in JavaScript:

// This
returnSomeOtherNumber(5) 
// evaluates to 10, for example, taking the value for output from its outer scope
// Became this
returnSomeOtherNumber(5) 
// evaluates to 5, input equal to output now

This can be fixed with renaming (alpha-conversion):

λz.y[y:=x] = λz.(y[y:=x]) = λz.x

Now there is no “name collisions” in our arguments.

Beta-reduction

Beta-reduction is a process of applying variable to a function. Basically, it can be viewed as a () operator in math and programming languages. You call a function with an argument to produce something, like multiplyByFive(2), which will evaluate to 10.

As a beta-reduction it would look like this (supposed we already defined numbers and multiplication function):

(λx.x * 5) 2 -> 5 * 2 -> 10

In a more general form (using substitution):

(λV.M) N is M[V := N]

Looks ominous in that form, but it’s actually can be read like “when applying function to a term, take function’s body and run it with applied argument as an input”.

Beta-reduction is very important in lambda calculus because it gives it that sweet Turing completeness and makes it a programming language.

Recursion

Recursion is the definition of a function using the function itself. But how do you create that in a language where every function is anonymous? Simple, you describe a function and then describe it again in its argument. Like that:

Y := λz.(λx.z (x x)) (λx.z (x x))

It’s a Y combinator (fix-point combinator), you’ve seen it in the beginning of this article, and it’s a recursion in lambda calculus. So, if you see Y and some term after it, it means that it will be recursively applied to itself with some argument.

I really like Y-combinator because it gives us an understanding of how recursion fundamentally works in programming and in nature itself in the form of self-replication (in DNA, for example). We can even say that it’s a simple representation of a code that drives the life itself, life of every living being on our planet.

Conclusion

So here we are. I hope you have enjoyed our journey and learned something new on the way. I’d like to believe that lambda calculus became a little bit clearer and closer to you as a concept of programming and reasoning, and you are inspired to learn more about it.

Here’s the list of things about lambda calculus we have covered today:

• variables
• functions
• lambda terms
• application
• abstraction
• free and bound variables
• alpha-conversion
• currying
• encoding datatypes
• substitution
• freshness condition
• beta-reduction
• Y-combinator (fix-point combinator)

And here’s the list of some things you can learn to deepen your understanding of the lambda calculus:

• more research on the topics above
• notations
• typed and untyped lambda calculus
• normal forms
• De Bruijn indexing (to eliminate alpha-conversion)
• η-reduction
• alpha equivalence
• undecidability of functional equivalence
• reduction strategies

If you have any questions, feel free to leave a comment here or contact me through my website (link in my Medium profile -> “How to contact me?”). I’ll be happy to help you.

Thank you for reading and joining me on this journey!