✓ Introduction to Lambda Calculus

Lambda Calculus (LC) is a rigorious mathematical system. It’s quite unique, and surprisingly powerful. So much of modern functional programming languages are directly based on LC.

LC is a system that describes functions and their actions.



  • Names are symbols that will represent unspecified value or function.

  • Names can be any string: fred, 12, x, y, \(\dots\)


An expression can be:

  • a name

  • a function abstraction

  • a function application

Abstraction and application expressions are to be defined.


Abstractions are of the form \((\lambda x.e)\) where

  • \(x\) is a name,

  • \(e\) is any expression.

\[\left(\lambda\underbrace{\mathbf{name}}_\mathrm{bound\ variable}.\ \underbrace{\mathbf{expression}}_\mathrm{body}\right)\]


Applications are of the form \((e_1 e_2)\) where

  • \(e_1\) and \(e_2\) are any expressions.

Some notation

  • \(\mathrm{Names}\) is the set of all possible names.

  • \(\mathrm{LC}\) is the set of all possible expressions which can be formally defined by induction as:

    • \(x\in\mathrm{Names}\implies x\in\mathrm{LC}\)

    • \(x\in\mathrm{Names}\) and \(e\in\mathrm{LC}\) \(\implies\) \((\lambda x.e)\in\mathrm{LC}\).

    • \(e_1, e_2\in\mathrm{LC}\) \(\implies\) \((e_1 e_2)\in\mathrm{LC}\).


The following are examples of \(\lambda\)-Calculus expressions.

Just a name


An application

\((x\ y)\)

Declaring the identity function

\((\lambda x.x)\)

Projection to the “first” parameter


Some interesting LC expression

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

Semantics of LC

  • All expressions represent functions.

  • Abstraction expression \(\lambda x.e\), where \(x\in\mathrm{Names}\) and \(e\in\mathrm{LC}\), describe functions that accept one argument \(x\), and return the result of its body expression \(e\).

  • Application expression \((e_1 e_2)\) evalues the function represented by \(e_1\) when its argument is \(e_2\).


Declaring curried functions

Currying is to construct nested functions, each is taking only one argument, but the body of the inner functions depend on the arguments of the outter functions. This can be done in LC with function abstractions.

For example:

\[(\lambda x.(\lambda y.(x y)))\]

As a matter of brevity, we omit the parentheses whenever it is clear.

\[(\lambda x.(\lambda y.(x y))) \longrightarrow \lambda x.\lambda y.(x y)\]

Using curried functions

Currying is a way for us to simulate functions with multiple inputs using nested function declarations involving single input functions.

To make use of curried function, we use repeated function application.

Suppose we have:

\[ f = \lambda x.\lambda y.\lambda z.\mathrm{body} \]

We can invoke \(f\) with parameters \(a\), \(b\), \(c\) as:

\[(((f\ a)\ b)\ c)\]

When dealing with multiple inputs done via currying, for readability, we will drop the parentheses.

So, for brevity, we have

\[ (((f\ a)\ b)\ c) \longrightarrow (f\ a\ b\ c) \]