Lambda Calculus

Lambda calculus is a simple and powerful notation for defining functions. Among its uses are

foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala
basis of higher order logic

In lambda calculus, functions have no side effects

they are mathematical functions from arguments to results
lambda calculus also supports higher-order functions
this model is appropriate for studying type checking
directly applicable to purely functional languages (like Haskell)

Anonymous Functions in Lambda Calculus

A function which takes its argument and increments it by 2 is given by lambda expression $\lambda x.x+2$ . The $\lambda$ operator is a binder used to indicate that a variable is to be treated as an argument of a function. We indicate function application by juxtaposition, writing $(f x)$ instead of $f(x)$ . Here are some example expressions and their values:

$\begin{equation*}\begin{array}{l} (\lambda x:int. x + 2)\, 7 = 9 \\ ((\lambda x:int. (\lambda y:int. x - y))\, 5)\, 3 = (\lambda y. 5 - y) 3 = 5 - 3 = 2 \\ (((\lambda f:int \to int. (\lambda x:int. f(f x))) (\lambda y:int. y^2))) 3 = (\lambda x. (\lambda y. y^2) ((\lambda y.y^2) x))) 3 = (\lambda y. y^2) ((\lambda y.y^2) 3) = (\lambda y.y^2) 9 = 81 \end{array} \end{equation*}$

Concrete syntax for $(\lambda x.x+2)5$ :

Isabelle theorem prover: '(% x.x+2)5' or '(\<lambda> x.x+2)5'
ocaml: '(function x → x+2)5'
Haskell: '(\ x → x+2)5'
Scala ((x:int) => x+2)(5)

Lambda Expressions

Abstract syntax of lambda expressions:

$\begin{equation*}\begin{array}{l} E ::= v \mid \lambda v:T.E \mid E\, E \\ v ::= v_1 \mid v_2 \mid ... \end{array}\end{equation*}$

That is, an expression is 1) a variable, 2) a lambda expression defining a function, or 3) an application of one expression to another.

Certain predefined variables are called constants (e.g. 7, 42, 13, but also operations +, *).

Types are given by the following grammar:

$\begin{equation*}\begin{array}{l} T ::= P \mid T \to T \\ P ::= \mbox{int} \mid \mbox{bool} \end{array} \end{equation*}$

There can be additional primitive types $P$ .

Currying

Instead of

$\begin{equation*} {+} : \mbox{int} \times \mbox{int} \to \mbox{int} \end{equation*}$

we have

$\begin{equation*} {+} : \mbox{int} \to (\mbox{int} \to \mbox{int}) \end{equation*}$

Therefore $(+ 2)$ is a function that increments its argument by $+$

expression $(+\ 2\ 7)$ is just a shorthand for $((+\ 2)\ 7)$

This is called currying in the honor of Haskell Curry

In general, instead of function

$\begin{equation*} f : T_1 \times T_2 \times \ldots \times T_n \to T \end{equation*}$

we can use function

$\begin{equation*} f : T_1 \to (T_2 \to \ldots \to (T_n \to T) \ldots) \end{equation*}$

Beta Reduction

The main rule of lambda calculus is beta reduction, which formalizes function application:

$\begin{equation*} (\lambda x. e_1) e_2 = e_1[x:=e_2] \end{equation*}$

Here we assume capture-avoiding substitution

we do renaming to avoid name clashes

Example:

$\begin{equation*}\begin{array}{l} ((\lambda y. (\lambda x. x + y)) 5) 7 = (\lambda x. x + 5) 7 = 7 + 5 \\ ((\lambda y. (\lambda x. x + y)) x) 7 \neq (\lambda x. x + x) 7 = 7 + 7 \\ ((\lambda y. (\lambda x. x + y)) x) 7 = ((\lambda y. (\lambda x'. x' + y)) x) 7 = (\lambda x'. x' + x) 7 = 7 + x \end{array} \end{equation*}$