Contents

✓ 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.

Definition

Names

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

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

Expression

An expression can be:

  • a name

  • a function abstraction

  • a function application

Abstraction and application expressions are to be defined.

Abstraction

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)\]

Application

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}\).

Example

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

Just a name

\(x\)

An application

\((x\ y)\)

Declaring the identity function

\((\lambda x.x)\)

Projection to the “first” parameter

\((\lambda\mathrm{first}.(\lambda\mathrm{second}.\mathrm{first}))\)

Can you decipher the expression?

Hint:

  1. \((x y)\) is evaluating \(x\) with \(y\) as the input.

  2. \(\lambda x. (x y)\) is the apply function.

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\).

Currying

The name refers to the logician Haskell Curry.

See https://en.wikipedia.org/wiki/Currying

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)))\]

The \(\lambda.\_\) is right associative, in the sense that the right most \(\lambda.\_\) takes precedence.

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.

The parameters are left associative, in the sense that the left most parameter takes precedence.

So, for brevity, we have

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