Lambda calculus provides some of the foundational structures that functional programming is built from. It therefore seems fitting to start my journey through functional programming with a thorough examination of lambda calculus. This first post will introduce Lambda calculus with references to the book An Introduction to Functional Programming Through Lambda Calculus.

Syntax

The complete syntax for Lambda calculus is surprisingly small and comprehensible. This section lists the syntax in its entirety, while following sections break the syntax down to explain each part.

$$ \begin{aligned} \langle expression \rangle & ::= \langle name \rangle | \langle function \rangle | \langle application \rangle \cr \langle name \rangle & ::= \text{non-blank character sequence} \cr \langle function \rangle & ::= \lambda \langle name \rangle \dot \langle body \rangle \cr \langle body \rangle & ::= \langle expression \rangle \cr \langle application \rangle & ::= ( \langle expression \rangle \langle expression \rangle ) \end{aligned} $$

Expression

$$ \langle expression \rangle ::= \langle name \rangle | \langle function \rangle | \langle application \rangle $$

Lambda calculus is a calculation system built around the evaluation of expressions (lambda expressions). A lambda expression can be either a name, which serves as an abstraction to refer to something else, a function, which defines the relationship between arguments and return values, and a function application, which executes the function for a certain set of arguments.

Name

$$ \langle name \rangle ::= \text{non-blank character sequence} $$

Names are simply character sequences. \(\text{kevin}\), \(\text{frog}\), \(\text{x}\), and \(\text{beta1}\) are all valid names.

Function

$$ \langle function \rangle ::= \lambda \langle name \rangle \dot \langle body \rangle $$

Functions are a bit more complicated. Michaelson states that a lambda function serves as an abstraction over a lambda expression, which isn’t that informative unless we take some time to understand what abstraction actually means.

Programmers use abstraction all the time by generalizing from a specific instance of a problem to a parameterized version of it. Abstraction uses names to refer to concrete objects or values (you can call them parameters if you like), as a means to create generalizations of specific problems. You can then take this abstraction (you can call it a function if you like), and replace the names with concrete objects or values to create a particular concrete instance of the problem. Readers familiar with refactoring can view abstraction as an “Extract Method” refactoring that turns a fragment of code into a method with parameters that explain the purpose of the method. For example,

void printOwing(double amount) {
  printBanner();

  System.out.println("name:" + this.name);
  System.out.println("name:" + amount);
}

$$ \Downarrow $$

void printOwing(double amount) {
  printBanner();
  printDetails(amount);
}

void printDetails(double amount) {
  System.out.println("name:" + this.name);
  System.out.println("name:" + amount);
}

In the preceding example, the printDetails method is an abstraction of a particular problem. Calling this abstraction with a particular value for the variable amount will turn the abstraction into a specific instance of the method (the one that prints this particular amount).

In mathematics, abstraction is created by replacing concrete values with names. For example, multiplication of concrete numbers uses the numbers themselves to perform the calculation:

$$ 7 \times 6 = 42 $$

You can generalize multiplication by replacing the concrete numbers with named symbols to create a function:

$$ f(x,y) = x \times y $$

And finally, you can apply this function substituting concrete values for the named parameters. By substituting \(7\) for \(x\) and \(6\) for \(y\) you can return to the concrete multiplication operation you began with:

$$ f(7,6) = 7 \times 6 = 42 $$

This may seem trivial (and it is), but lambda calculus is based entirely on using function abstraction to generalize expressions by introducing names (variables), and function application to evaluate a previously generalized expression using particular values in place of names. With this background in place, we can start to examine more closely the original definition of a lambda function.

$$ \langle function \rangle ::= \lambda \langle name \rangle . \langle body \rangle $$

The symbol \(\lambda\) introduces the function by the \(\langle name \rangle\) that succeeds it. The name can be treated as the formal parameter to the function so \(\lambda(x)\) is roughly equivalent to \(f(x)\) in comparison to traditional mathematics. The \(\langle name \rangle\) is technically called the lambda function’s bound variable — the variable name will be bound to whatever value you use when the function is called. The \(.\) syntax separates the bound variable from the function’s body. The body is the functional abstraction that can make use of the bound variable to perform whatever computation you specify. Let’s now revisit the definitions to define what a function body actually is.

Body

$$ \langle body \rangle ::= \langle expression \rangle $$

If a function’s body simply returned a concrete value, lambda calculus would not be different from traditional programming functions that take a formal parameter and use that parameter to perform a computation, returning a value. The key to lambda calculus is that the body can actually be any valid expression. Looking back at our definition for an expression we can see that a lambda function’s body can return another function or a function application. Although this distinction subtle, it is actually the source of the expressive power of lambda calculus.

Application

$$ \langle application \rangle ::= ( \langle expression \rangle \langle expression \rangle ) $$

An application is syntactically described as the combination of two expressions encased in brackets. Semantically, the first expression is called the function expression — the lambda function contain the parameter or bound variable. The second expression is the argument expression — the value to be supplied to the expression’s bound variable. Our specification for application can be redefined using this knowledge.

$$ \begin{aligned} \langle application \rangle & ::= ( \langle function \ expression \rangle \langle argument \ expression \rangle ) \cr \langle function \ expression \rangle & ::= \langle expression \rangle \cr \langle argument \ expression \rangle & ::= \langle expression \rangle \end{aligned} $$

An application therefore specializes an abstract function by providing a value for the named variable. The key difference between this definition of function application in comparison to traditional programming languages is that lambda calculus allows for function definitions to be defined directly in front of function calls.

When a function application is performed, it is said to be evaluated, and there are two ways in which an application can be evaluated. In both cases, we first start by evaluating the function expression to return a function that takes bound variables or parameters. Then we can replace all of the bound variables with the argument expression in one of two ways:

  1. the evaluated argument expression
  2. the unevaluated argument expression

The first approach is called applicative order reduction and is similar to a pass-by-value approach to function evaluation in imperative programming languages. With this approach, the value of each parameter is evaluated and known at the time when the function body is executed. The second approach is called normal order reduction and is similar to a pass-by-reference approach in imperative programming languages. Here, the argument expression is substituted with the bound variable directly and without evaluation. Normal order reduction allows for lazy evaluation which is a subject for another day. In either case, after this replacement takes place, the body expression is evaluated. Both applicative order or normal order reduction result in the same final value of a function call.

Some Examples

So far, we’ve covered a lot of theory. Let’s put this theory into practice by looking at a few example lambda expressions and their evaluation. You can refer back to the syntax and semantics to help understand any examples that may seem tricky. A key point to remember is that lambda calculus only allows two things: abstraction via the creation of a function expression, and specialization via the application of a function expression to an argument expression.

Simple Example: The Identity Function

The identity function is expressed very simply as

$$ \lambda x.x $$

We can take this syntax and break it down into its component pieces. The symbol lambda is the signal to start an abstraction (function). The first occurrence of \(x\) is the formal parameter to the function — also known as the abstraction’s bound variable. The \(.\) is a syntactical separator between the formal parameter and the abstraction’s body. The last occurrence of \(x\) is the abstraction’s body.

We can trigger an evaluation of this function by wrapping it in brackets and providing an argument expression:

$$ (\lambda x.x \ y) $$

Here, the bound variable (before the \(.\)) is \(x\), and the body expression (after the \(.\)) is also \(x\). The argument expression is \(y\). When the function is applied, the bound variable \(x\) is replaced by the argument expression \(y\) wherever it is used in the body expression. For the identity function, you replace the body expression with the argument expression, resulting in \(y\). Following these steps,

$$ (\lambda x.x \ y) $$

becomes

$$ (\lambda y.y) $$

which is replaced by the body expression by application, becoming

$$ y $$

Expressing Arithmetic Using Lambda Calculus

All natural numbers can be represented using Church numerals that define zero and the successors to zero. For example, the number zero can be expressed as the name \(\text{zero}\), and the number one can be expressed as the successor of \(\text{zero}\), \(\text{suc}(\text{zero})\). Two is then \(\text{suc}(\text{suc}(\text{zero}))\) and so on.

In lambda calculus, everything is expressed using function application and specialization. This includes math. So we need to start by defining zero:

$$ 0 \equiv \lambda f . (\lambda x . x ) $$

Numbers can be extended to include \(1\), \(2\), and \(3\) by applying a function successively to the zero value.

$$ \begin{aligned} 1 & \equiv \lambda f . (\lambda x . f x) \cr 2 & \equiv \lambda f . (\lambda x . f (f x)) \cr 3 & \equiv \lambda f. (\lambda x .f (f (f x))) \end{aligned} $$

Each successive Church numeral applies the function expression \(f\) to the argument expression \(x\). In other words, the \(n\)-th Church numeral is a function that takes a function \(f\) as an argument that is composed on itself \(n\) times.

Conclusion

This post introduced the lambda calculus by defining its syntax and then examining each syntactical construct in detail. It concludes with some examples of applying lambda calculus. Most of the material in this post was poorly cobbled together using the book An Introduction to Functional Programming Through Lambda Calculus. If you want to really dive deep into the subject, go straight to that source.