lambda calculus


Lambda calculusMathworldPlanetmath (often referred to as λ-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.

λ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 λ-calculus is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to combinatory logicMathworldPlanetmath (though much more concise). Most functional programming languagesPlanetmathPlanetmath are also equivalent to λ-calculus, to a degree (any imperative features in such languages are, of course, not equivalent).

Examples

We can specify the Church integer 3 in λ-calculus as

3=λfx.f(f(fx))

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

3inc"0"="3"

AdditionPlanetmathPlanetmath of Church integers in λ-calculus is

add = λxy.(λfz.xf(yfz))
add 2 3 = λfz . 2f(3fz)
= λfz . 2f(f(f(fz)))
= λfz.f(f(f(f(fz))))
= 5
mul = λxy.(λfz.x(λw.yfw)z)
mul 2 3 = λfz . 2(λw . 3fw)z
= λfz . 2(λw.f(f(fw)))z
= λfz.f(f(f(f(f(fz)))))
= 6.

Russell’s Paradox in λ-calculus

The λ-calculus readily admits Russell’s ParadoxMathworldPlanetmath. 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=λx.not(xx)

Now what happens when we apply r to itself?

rr = not(rr)
= not(not(rr))

Since we have 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