## You are here

Homelambda calculus

## Primary tabs

# 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\;.\;f\;x$ |

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 f\;x\;.\;f\;(f\;(f\;x))$ |

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

$3\;\inc\;\texttt{"0"}=\texttt{"3"}$ |

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

$\displaystyle\add$ | $\displaystyle=$ | $\displaystyle\lambda\;x\;y\;.\;(\lambda\;f\;z\;.\;x\;f\;(y\;f\;z))$ | ||

$\displaystyle\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$ |

$\displaystyle\mul$ | $\displaystyle=$ | $\displaystyle\lambda\;x\;y\;.\;(\lambda\;f\;z\;.\;x\;(\lambda\;w\;.\;y\;f\;w)% \;z)$ | ||

$\displaystyle\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 $r$ that takes a function $x$ as an argument, and is reduced to the application of the logical function $\Not$ to the application of $x$ to itself.

$r\;=\;\lambda\;x\;.\;\Not\;(x\;x)$ |

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

$\displaystyle r\;r$ | $\displaystyle=$ | $\displaystyle\Not\;(r\;r)$ | ||

$\displaystyle=$ | $\displaystyle\Not\;(\Not\;(r\;r))$ | |||

$\displaystyle\vdots$ |

Since we have $\Not\;(r\;r)=(r\;r)$, we have a paradox.

## Mathematics Subject Classification

03B40*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff

## Recent Activity

new question: Prove that for any sets A, B, and C, An(BUC)=(AnB)U(AnC) by St_Louis

Apr 20

new image: information-theoretic-distributed-measurement-dds.png by rspuzio

new image: information-theoretic-distributed-measurement-4.2 by rspuzio

new image: information-theoretic-distributed-measurement-4.1 by rspuzio

new image: information-theoretic-distributed-measurement-3.2 by rspuzio

new image: information-theoretic-distributed-measurement-3.1 by rspuzio

new image: information-theoretic-distributed-measurement-2.1 by rspuzio

Apr 19

new collection: On the Information-Theoretic Structure of Distributed Measurements by rspuzio

Apr 15

new question: Prove a formula is part of the Gentzen System by LadyAnne

Mar 30

new question: A problem about Euler's totient function by mbhatia