LARA

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*}

Variable Capture

Rules for Constants

For each constant we have appropriate rule, for example we have

\begin{equation*}
    ({+}\ 3\ 5) = 8
\end{equation*}

and so on, for each pair of integer constants. Similarly,

\begin{equation*}
    (and\ true\ false) = false
\end{equation*}

we can introduce conditional constant $ite$, writing $(ite\ e_1\ e_2)$, with rules

\begin{equation*}\begin{array}{l}
   (ite\ true\ e_1\ e_2) = e_1 \\
   (ite\ false\ e_1\ e_2) = e_2 \\
\end{array}
\end{equation*}

and so on.

If we get something like

\begin{equation*}
   ({+}\ true\ 5)
\end{equation*}

this is a run-time type error

  • program would crash at run-time or produce bad result
  • we introduce a type system to avoid this