PlanetMath: lambda calculus

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (211)
Orphanage
Unclass'd (1)
Unproven (472)
Corrections (36)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

Entry average rating: No information on entry rating

lambda calculus

(Definition)

Lambda calculus (often referred to as $\lambda$ -calculus) was invented in the 1930s by Alonzo Church, as a form of mathematical logic dealing primarly with functions and the application of functions to their arguments. In pure lambda calculus, there are no constants. Instead, there are only lambda abstractions (which are simply specifications of functions), variables, and applications of functions to functions. For instance, Church integers are used as a substitute for actual constants representing integers.

A lambda abstraction is typically specified using a lambda expression, which might look like the following.

$\displaystyle \lambda\;x\;.\;f\;x$

The above specifies a function of one argument, that can be reduced by applying the function to its argument (function application is left-associative by default, and parentheses can be used to specify associativity).

The $\lambda$ -calculus is equivalent to combinatory logic (though much more concise). Most functional programming languages are also equivalent to $\lambda$ -calculus, to a degree (any imperative features in such languages are, of course, not equivalent).

Examples

We can specify the Church integer in $\lambda$ -calculus as

$\displaystyle 3 = \lambda f\;x\;.\;f\;(f\;(f\;x))$

Suppose we have a function ${\mathrm{inc}}$ , which when given a string representing an integer, returns a new string representing the number following that integer. Then

$\displaystyle 3\;{\mathrm{inc}}\;\texttt{''0''} = \texttt{''3''}$

Addition of Church integers in $\lambda$ -calculus is

$\displaystyle {\mathrm{add}}$	$\displaystyle =$	$\displaystyle \lambda\;x\;y\;.\;(\lambda\;f\;z\;.\;x\;f\;(y\;f\;z))$
$\displaystyle {\mathrm{add}}\;2\;3$	$\displaystyle =$	$\displaystyle \lambda\;f\; z\; .\; 2\; f\; (3\; f\; z)$
	$\displaystyle =$	$\displaystyle \lambda\; f\; z\; .\; 2\; f\; (f\; (f\; (f\; z)))$
	$\displaystyle =$	$\displaystyle \lambda\; f\; z\; .\; f\; (f\; (f\; (f\; (f\; z))))$
	$\displaystyle =$	$\displaystyle 5$

Multiplication is

$\displaystyle {\mathrm{mul}}$	$\displaystyle =$	$\displaystyle \lambda\;x\;y\;.\;(\lambda\;f\;z\;.\;x\;(\lambda\;w\;.\;y\;f\;w)\;z)$
$\displaystyle {\mathrm{mul}}\;2\;3$	$\displaystyle =$	$\displaystyle \lambda\;f\;z\;.\;2\;(\lambda\;w\;.\;3\;f\;w)\;z$
	$\displaystyle =$	$\displaystyle \lambda\;f\;z\;.\;2\;(\lambda\;w\;.\;f\;(f\;(f\;w)))\;z$
	$\displaystyle =$	$\displaystyle \lambda\;f\;z\;.\;f\;(f\;(f\;(f\;(f\;(f\;z)))))$
	$\displaystyle =$	$\displaystyle 6.$

Russell's Paradox in $\lambda$ -calculus

The $\lambda$ -calculus readily admits Russell's Paradox. Let us define a function that takes a function as an argument, and is reduced to the application of the logical function ${\mathrm{not}}$ to the application of to itself.

$\displaystyle r\;=\;\lambda\;x\;.\;{\mathrm{not}}\;(x\;x)$

Now what happens when we apply to itself?

$\displaystyle r\;r$	$\displaystyle =$	$\displaystyle {\mathrm{not}}\;(r\;r)$
	$\displaystyle =$	$\displaystyle {\mathrm{not}}\;({\mathrm{not}}\;(r\;r))$
	$\displaystyle \vdots$