Chapter 1: Introduction

Overview

The lambda calculus can be thought of as the theoretical foundation of functional programming. It is a Turing complete language.

The lambda calculus expressions ($\Lambda$) consist of following three types of elements:

$$\begin{array}{lll} \text{Variables: }&\text{If } x \text{ is a variable, then }& x\in\Lambda\\ \text{Abstractions: }&\text{If } x \text{ is a variable, and } M \in \Lambda \text{, then }& \lambda x. M\in\Lambda\\ \text{Applications: }&\text{If } M \in \Lambda \text{ and } N \in \Lambda \text{, then }& M N\in\Lambda\\ \end{array}$$

Don't worry about obscure mathematical definition above, let's learn it by examples.

Lambda Function

Let's take an anonymous function for example:

$$x^2$$

Substitute $7$ for $x$:

$$x^2|_{x=7}=49$$

Similar function donated in lambda calculus requires explicit indication of parameter as:

$$\lambda x.x^2$$

Substitution is renamed to application with another syntax similar to multiplication in regular mathematics:

$$(\lambda x.x^2)7=49$$

A name could also be assigned to the function like this:

$$f(x)=x^2\\ f(7)=49$$

In lambda calculus, it should be rewritten as:

$$f=\lambda x.x^2\\ f7=49$$

At the first glance, you may be confused. Don't worry, let's check it in detail.

Compare following two expressions:

$$x=7\\ f=\lambda x.x^2$$

We may say, $x$ is a variable, whose value equals $7$.

Similarly, let's say, $f$ is also a variable, whose value equals a function.

It reveals one of core ideas about lambda calculus. That is, functions are also variables. You will get accustomed to this soon.

There are some conventions of named functions. For example:

$$I=\lambda x.x$$

Identity function $I$ returns its parameter unchanged. It will be mentioned again later.

Function as Return Value

Since now functions are also variables, please view following example:

$$f=\lambda x.\lambda y.(x+y)\\ f3=\lambda y.(3+y)\\ (f3)4=3+4=7$$

$f$ is a function whose return value is also a function. Just like normal value functions, whose return value is determined by its parameters, the function returned by $f$ is also determined by its parameter $x$. $f3$ is "plus 3 function" and $f4$ is "plus 4 function". Then we may apply it again with another parameter to obtain further result.

Free variables are those whose value is not determined by its direct enclosing function. Free variable of inner function taking the value from outer function is called capture.

Currying and Uncurrying

If we treat consecutive lambda function chain as one multiple-parameter function:

$$\lambda x.\lambda y.\lambda z.M\overset{\text{uncurrying}}{\underset{\text{currying}}{\rightleftarrows}}\lambda xyz.M$$

We may review the previous example from another perspective:

$$\begin{array}{lr} f=\lambda xy.(x+y)\\ f\space3=\lambda y.(3+y)&(2)\\ f\space 3\space 4=3+4=7 \end{array}$$

Pay attention to the line $(2)$. It partially applies the function with only first parameter and yields a function taking successive ones, which is called partial application. In fact, the definition of partial application of uncurrying multiple-parameter function is exactly corresponding to the practice of application of currying consecutive lambda function chain - as if it is.

From the one perspective of associativity, application is also similar to multiplication in regular mathemtics just as syntax do - contiguous operands should be applied from left to right. That is,

$$ABC=(AB)C$$

represents apply $A$ with $B$, and apply previous result with $C$.

From the other persepctive of currying and uncurrying, left side of equation reprensents apply $A$ with $B$ together and right side of equation represents apply it step by step. But at the end of day, they are equivalent and no more than two different ways to understand the same application process.

Function as Parameter

Similarly, functions could be passed as parameters, too:

$$F=\lambda fx.fxx\\ f=\lambda xy.(x+y)\\ \begin{array}{} Ff2&=&(\lambda fx.fxx)(\lambda xy.(x+y))2\\&=&(\lambda xy.(x+y))2\space2\\&=&4 \end{array}$$

It is remarkable that $Ff$ produces a new function from an old one. Isn't it cool to manipulate functions instead of just values?

Reduction

To simplify lambda calculus expressions, three kinds of reductions will be introduced.

Alpha reduction

$$\lambda x.x = \lambda y.y$$

$\alpha$ reduction is also known as $\alpha$ equivalence. Substitution of parameter name does not change semantics. It is similar to following cases in regular mathematics:

$$f(x)=x^2\equiv f(y)=y^2\\$$ $$\int_0^1ug(u)du=\int_0^1vg(v)dv$$ $$\sum_{i=1}^\infty a_i=\sum_{j=1}^\infty a_j$$

Note despite semantics unchanged, name conflicts and shadowing may casue ambiguity and confusion:

$$\lambda x.\lambda y.y=\lambda x.\lambda x.x\space?$$

It is more damaging than those cases in regular mathematics:

$$F(x)=\int_{-\infty}^xf(x)dx$$

Beware outer $x$ and inner $x$ are differnet ones.

Beta reduction

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

This is exactly what application is all about. Most common reduction during lambda calculus is the $\beta$ reduction.

Note that a constant function cannot be reduced to the constant even if the constant is independent from the parameter. An application is necessary.

$$\lambda x.c\neq c\\ (\lambda x.c)y= c\\$$

Eta reduction

$$\lambda y.xy=x$$

$\eta$ reduction is not that obvious. To prove this equation, we'd better introduce a helper variable $z$ to be applied with:

$$(\lambda y.xy)z=xz$$

Applying them with identical parameter yield identical result. That's why they are considered equivalent.