# lambda calculus

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

$$\lambda x.fx$$ |

The above specifies a function of one argument, that can be *reduced* by applying the function $f$ 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 $3$ in $\lambda $-calculus as

$$3=\lambda fx.f(f(fx))$$ |

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

$$3\mathrm{inc}\mathtt{\text{"0"}}=\mathtt{\text{"3"}}$$ |

Addition^{} of Church integers in $\lambda $-calculus is

$\mathrm{add}$ | $=$ | $\lambda xy.(\lambda fz.xf(yfz))$ | ||

$\mathrm{add}\mathrm{\hspace{0.33em}2\hspace{0.33em}3}$ | $=$ | $\lambda fz\mathrm{\hspace{0.33em}.\hspace{0.33em}2}f(3fz)$ | ||

$=$ | $\lambda fz\mathrm{\hspace{0.33em}.\hspace{0.33em}2}f(f(f(fz)))$ | |||

$=$ | $\lambda fz.f(f(f(f(fz))))$ | |||

$=$ | $5$ |

$\mathrm{mul}$ | $=$ | $\lambda xy.(\lambda fz.x(\lambda w.yfw)z)$ | ||

$\mathrm{mul}\mathrm{\hspace{0.33em}2\hspace{0.33em}3}$ | $=$ | $\lambda fz\mathrm{\hspace{0.33em}.\hspace{0.33em}2}(\lambda w\mathrm{\hspace{0.33em}.\hspace{0.33em}3}fw)z$ | ||

$=$ | $\lambda fz\mathrm{\hspace{0.33em}.\hspace{0.33em}2}(\lambda w.f(f(fw)))z$ | |||

$=$ | $\lambda fz.f(f(f(f(f(fz)))))$ | |||

$=$ | $6.$ |

## Russell’s Paradox in $\lambda $-calculus

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

$$r=\lambda x.\mathrm{not}(xx)$$ |

Now what happens when we apply $r$ to itself?

$rr$ | $=$ | $\mathrm{not}(rr)$ | ||

$=$ | $\mathrm{not}(\mathrm{not}(rr))$ | |||

$\mathrm{\vdots}$ |

Since we have $\mathrm{not}(rr)=(rr)$, we have a paradox.

Title | lambda calculus |

Canonical name | LambdaCalculus |

Date of creation | 2013-03-22 12:32:39 |

Last modified on | 2013-03-22 12:32:39 |

Owner | ratboy (4018) |

Last modified by | ratboy (4018) |

Numerical id | 9 |

Author | ratboy (4018) |

Entry type | Definition |

Classification | msc 03B40 |

Related topic | CombinatoryLogic |

Related topic | ChurchInteger |

Related topic | RussellsParadox |

Defines | pure lambda calculus |

Defines | lambda abstraction |

Defines | lambda expression |