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{align*} \langle expression \rangle & ::= \langle name \rangle | \langle function \rangle | \langle application \rangle \\ \langle name \rangle & ::= \text{non-blank character sequence} \\ \langle function \rangle & ::= \lambda \langle name \rangle \dot \langle body \rangle \\ \langle body \rangle & ::= \langle expression \rangle \\ \langle application \rangle & ::= ( \langle expression \rangle \langle expression \rangle ) \\ \end{align*} \]

## 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 (λ expressions). A λ 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. `kevin`

, `frog`

, `x`

, and `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 λ function serves as an abstraction over a λ 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 λ 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 λ function.

\[ \langle function \rangle ::= \lambda \langle name \rangle . \langle body \rangle \]

The symbol λ introduces the function by the `<name>`

that succeeds
it. The name can be treated as the formal parameter to the function so
λ(x) is roughly equivalent to `f(x)`

in comparison to traditional
mathematics. The `<name>`

is technically called the λ 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, λ 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 λ calculus is that the body can
actually be *any* valid expression. Looking back at our definition for an
expression we can see that a λ 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 λ 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 λ 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{align*} \langle application \rangle & ::= ( \langle function \ expression \rangle \langle argument \ expression \rangle ) \\ \langle function \ expression \rangle & ::= \langle expression \rangle \\ \langle argument \ expression \rangle & ::= \langle expression \rangle \\ \end{align*} \]

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 λ 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:

- the evaluated argument expression
- 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 λ 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 λ 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 λ 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 `zero`

, and the number one can be expressed as the successor
of `zero`

, `suc(zero)`

. Two is then `suc(suc(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{align*} 1 & \equiv \lambda f . (\lambda x . f x) \\ 2 & \equiv \lambda f . (\lambda x . f (f x)) \\ 3 & \equiv \lambda f. (\lambda x .f (f (f x))) \\ \end{align*} \]

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 λ calculus by defining its syntax and then examining each syntactical construct in detail. It concludes with some examples of applying λ 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.