Differences
This shows you the differences between two versions of the page.
lambda_calculus [2007/05/28 21:18] vkuncak |
lambda_calculus [2015/04/21 17:32] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Lambda calculus ====== | ||
- | This is a very brief introduction to lambda calculus. | ||
- | |||
- | Lambda calculus is a notation for defining functions. It is very simple and powerful. Two of its main uses are | ||
- | * foundation of programming languages, especially functional languages such as Ocaml, Haskell, and Scala | ||
- | * higher order logic notations, such as Isabelle, HOL, PVS | ||
- | |||
- | For example, 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. Here are some example expressions and their values: | ||
- | \begin{eqnarray*} | ||
- | (\lambda x. x + 2)\, 7 &=& 9 \\ | ||
- | ((\lambda x. (\lambda y. x - y))\, 5)\, 3 &=& (\lambda y. 5 - y) 3 = 5 - 3 = 2 \\ | ||
- | (((\lambda f. (\lambda x. f(f x))) (\lambda y. 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{eqnarray*} | ||
- | |||
- | Note: in Isabelle and Jahob notation we use '% x.F' or '\<lambda> x.F' to denote $\lambda$.F binder. In [[http://caml.inria.fr|ocaml]], one can use 'function x -> F', and in [[http://www.haskell.org|Haskell]] one can use '\ x -> F'. | ||
- | |||
- | ===== Lambda expressions ===== | ||
- | |||
- | Untyped lambda expressions are given by following grammar: | ||
- | \begin{equation*} | ||
- | T ::= v \mid \lambda v.T \mid T\, T \\ | ||
- | v ::= v_1 \mid v_2 \mid ... | ||
- | \end{equation*} | ||
- | That is, an expression is a variable, a lambda expression defining a function, or an application of one expression to another. | ||
- | |||
- | ===== Beta reduction ===== | ||
- | |||
- | The main rule of lambda calculus is beta reduction, which formalizes function application: | ||
- | \begin{equation*} | ||
- | (\lambda x. s) t = s[x:=t] | ||
- | \end{equation*} | ||
- | where we assume capture-avoiding substitution. | ||
- | |||
- | One simple use of lambda expressions to introduce shorthands: instead of writing | ||
- | \begin{equation*} | ||
- | \mbox{let}\ x = E\ \mbox{in}\ F | ||
- | \end{equation*} | ||
- | we can write | ||
- | \begin{equation*} | ||
- | (\lambda x.F)E | ||
- | \end{equation*} | ||
- | |||
- | References: | ||
- | * Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984) ([[http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html|Chad Brown's notes on this book]]) |