What is the lambda (λ) calculus?
by Liger Learn
This article is part of a series of articles on the lambda calculus and is also available as a YouTube video.
- (This article) What is the lambda (λ) calculus?
- Bound vs. free variables in the lambda (λ) calculus
- Delta (δ) rules in the lambda (λ) calculus
- Beta (β) reduction in the lambda (λ) calculus
- Alpha (α) conversion in the lambda (λ) calculus
- Eta (η) conversion in the lambda (λ) calculus
- Summary of the lambda calculus (λ) evaluation rules
- Lambda calculus (λ) reduction orders and normal form
- The Church-Rosser theorem and the lambda (λ) calculus
So, what exactly is the lambda calculus? The lambda calculus (λ-calculus) is a formal system for expressing computation developed by Alonzo Church. Church was in 1903 and died in 1995 in the United States. It’s called the lambda calculus because the Greek letter lambda, λ, is used to define expressions and terms within the system (as we will see later). It is often useful to think of the lambda calculus as a sort of “assembly language” for functional languages. This is because higher level functional programming languages like Haskell, Ocaml and others usually translate their source code into an intermediate form of one of the many variants of lambda calculus. There are many variants of the lambda calculus which exist, including:
- The simple untyped lambda calculus.
- The simple typed lambda calculus.
- System F, the polymorphic lambda calculus.
- System Fω, a variant of system F with type operators.
- And others..
Defining a function as a λ-abstraction“Lambda abstraction” is the term used within the lambda calculus for a function. Consider the following traditional mathematical function: \[f(x) = x + 1\] This defines a function called f which has a single argument x and the function body simply adds 1 to x. And you apply an argument to the function like so: \[f(1) = 1 + 1 = 2\] Now let’s consider the lambda abstraction equivalent: \[\lambda x.(+\ x \ 1)\] This may look like an alien language, but that is fine – I’ll explain it:
- First, it starts with the lambda symbol, then an x, then a dot, and then the function body.
- The lambda symbol denotes that a lambda abstraction is being defined.
- The x is the formal parameter to the lambda abstraction.
- Then within the brackets is the function body:
- In the lambda calculus function application is always written in the prefix form. So the + is always before its arguments.
- It might be a bit weird to see at first because we are taught to place the plus operator in an infix position in mathematics classes but you will get used to it after a while.
The simple untyped lambda (λ) calculus definitionNow that we know what a lambda abstraction is we can look at the actual definition of the lambda calculus. The image below (labelled Figure 2.1) contains the definition*: This definition is written in BNF which stands for Backus–Naur form. This is a simple way of describing the syntax of a language. The symbol “colon colon equals” (::=) can be read as “is defined as” and the pipe symbol (|) can be read as “or”. Anything within the less than (<) and greater than (>) signs is a name for a class of symbol within the language. So we can see that the lambda calculus is a language which allows you to define an <exp> (expression) where an expression is defined as: a constant OR a variable OR an expression placed next to another expression, OR a lambda abstraction. Now you see why we covered what a lambda abstraction is earlier in the article. An important thing to note about this definition is that it is recursive – that means that the thing that we are defining, <exp> is defined in terms of itself. Also, for our definition of <constant> we are including all numbers, as well as built in arithmetic functions such as addition, multiplication, etc. We can slowly build up lambda calculus programs by starting with an <exp> and replacing it with one of the options on the right. Let’s walk through a simple example confirming that (* 3 4) is a valid lambda calculus expression:
- We always begin with the <exp>
- <exp> <exp>
- One of the definitions of an <exp> is two expressions next to each other (application), so we replace the <exp> with <exp> <exp>.
- We replace the first <exp> with <constant>, since one of the things an <exp> is defined as is a <constant>.
- * <exp>
- For our definition of <constant> we also include built in arithmetic functions, and so we can replace it with the multiplication function.
- * <exp> <exp>
- Just like from step 1 to 2 we replace the single <exp> with two next to each other.
- * <constant> <exp>
- We replace the first <exp> with <constant>.
- * 3 <exp>
- We swap the <constant> for the actual constant value 3.
- * 3 <constant>
- We replace the <exp> with a <constant>.
- * 3 4
- We replace the <constant> with the constant value 4.
- (* 3 4)
- We add brackets onto the final expression for grouping it together as one.
*The image of the definition of the untyped lambda calculus is taken from the book The Implementation of Functional Programming Languages (1987) authored by Simon Peyton Jones. The book itself is available for free from here.
October 19, 2023
October 19, 2023
October 19, 2023