Differences
This shows you the differences between two versions of the page.
sav08:untyped_lambda_calculus [2009/03/05 12:45] vkuncak |
sav08:untyped_lambda_calculus [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Untyped 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 | ||
- | |||
- | ===== Intuition ===== | ||
- | |||
- | 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*} | ||
- | |||
- | Concrete syntax for $(\lambda x.x+2)5$: | ||
- | * Isabelle (and Jahob): '(% x.x+2)5' or '(\<lambda> x.x+2)5' | ||
- | * [[http://caml.inria.fr|ocaml]]: '(function x -> x+2)5' | ||
- | * [[http://www.haskell.org|Haskell]]: '(\ x -> x+2)5' | ||
- | * [[http://www.scala-lang.org|Scala]]: '((x:int) => x+2)(5)' | ||
- | |||
- | ===== Lambda expressions ===== | ||
- | |||
- | Untyped lambda expressions are given by following grammar: | ||
- | \[\begin{array}{l} | ||
- | T ::= v \mid \lambda v.T \mid T\, T \\ | ||
- | v ::= v_1 \mid v_2 \mid ... | ||
- | \end{array}\] | ||
- | 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\ \mathop{\to}\limits^{\beta}\ s[x:=t] | ||
- | \end{equation*} | ||
- | where we assume capture-avoiding substitution. In general, we identify terms that differ only by renaming of fresh bound variables. | ||
- | |||
- | ===== Non-termination and Difficulties with Semantics ===== | ||
- | |||
- | Let $\omega$ denote term | ||
- | \[ | ||
- | (\lambda x.xx)(\lambda x.xx) | ||
- | \] | ||
- | Note that $\omega$ beta reduces to itself. It represents infinite loop. | ||
- | |||
- | Note that the set of total functions is not a model of untyped lambda calculus. Consider the self-application expression $x x$. Suppose the interpretation of variable $x$ ranges over a domain $D$. This domain should be a set of total functions $f : A \to B$ to enable application. But all possible values of $x$ are an argument, so we have that | ||
- | \[ | ||
- | D = [D \to D] | ||
- | \] | ||
- | that is, the set $D$ is equal to the set of all functions from $D$ to $D$. But this is not possible in set theory, because we can prove that the set $D^D$ has larger cardinality (even if it is infinite). For example, if $D$ is the set of natural numbers (which is countably infinite), then $D^D$ would be uncountably infinite. | ||
- | |||
- | The models of untyped lambda calculus do exist, but they usually consider only certain 'continuous', partial, functions. These domains are studied in //domain theory//. Roughly speaking, in domain theory, a solution to equation such as $D \simeq [D \leadsto D]$ is obtained by finding a fixpoint of a monotonic operator $F(D) = [D \leadsto D]$. | ||
- | |||
- | Thus, untyped lambda calculus is easy to understand syntactically (as a set of rules for manipulating formal expressions), rather than a system where each expression has some intuitive meaning. | ||
- | |||
- | References: | ||
- | * Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984) | ||
- | * [[http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf|Domain Theory]] and {{sav08:domaintheory.pdf|pdf file}} | ||