Lambda calculus

Lambda calculus consists of constructing lambda terms and performing reduction operations on them. In the simplest form of lambda calculus, terms are built using only the following rules:

Variable names are not needed if using a universal lambda function, such as Iota and Jot, which can create any function behavior by calling it on itself in various combinations.

There is some uncertainty over the reason for Church's use of the Greek letter lambda (λ) as the notation for function-abstraction in the lambda calculus, perhaps in part due to conflicting explanations by Church himself. According to Cardone and Hindley (2006):

This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and λ just happened to be chosen.

According to Scott, Church's entire response consisted of returning the postcard with the following annotation: "eeny, meeny, miny, moe".

This method, known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.

As described above, all functions in the lambda calculus are anonymous functions, having no names. They only accept one input variable, with currying used to implement functions of several variables.

The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid C programs and some are not. A valid lambda calculus expression is called a "lambda term".

The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms:

In lambda calculus, functions are taken to be 'first class values', so functions may be used as the inputs, or be returned as outputs from other functions.

There are several notions of "equivalence" and "reduction" that allow lambda terms to be "reduced" to "equivalent" lambda terms.

The following definitions are necessary in order to be able to define β-reduction:

(free variables in lambda Notation and its Calculus are comparable to )

The free variables of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively:

Another aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to truth values, strings, or other non-number objects.

To keep the notation of lambda expressions uncluttered, the following conventions are usually applied:

We also speak of the resulting equivalences: two expressions are α-equivalent, if they can be α-converted into the same expression. β-equivalence and η-equivalence are defined similarly.

In the De Bruijn index notation, any two α-equivalent terms are syntactically identical.

However, it can be shown that β-reduction is confluent when working up to α-conversion (i.e. we consider two normal forms to be equal if it is possible to α-convert one into the other).

Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.

The basic lambda calculus may be used to model booleans, arithmetic, data structures and recursion, as illustrated in the following sub-sections.

By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.

Then, with these two lambda terms, we can define some logic operators (these are just possible formulations; other expressions are equally correct):

The following predicate tests whether the first argument is less-than-or-equal-to the second:

which allows us to give perhaps the most transparent version of the predecessor function:

By chaining such definitions, one can write a lambda calculus "program" as zero or more function definitions, followed by one lambda-term using those functions that constitutes the main body of the program.

The self-application achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced and called there.

This solves it but requires re-writing each recursive call as self-application. We would like to have a generic solution, without a need for any re-writes:

The leftmost, outermost redex is always reduced first. That is, whenever possible the arguments are substituted into the body of an abstraction before the arguments are reduced.
The leftmost, innermost redex is always reduced first. Intuitively this means a function's arguments are always reduced before the function itself. Applicative order always attempts to apply functions to normal forms, even when this is not possible.
Any redex can be reduced at any time. This means essentially the lack of any particular reduction strategy—with regard to reducibility, "all bets are off".
A redex is reduced only when its right hand side has reduced to a value (variable or abstraction). Only the outermost redexes are reduced.

Strategies with sharing reduce computations that are "the same" in parallel:

As normal order, but computations that have the same label are reduced simultaneously.
As call by name (hence weak), but function applications that would duplicate terms instead name the argument, which is then reduced only "when it is needed".

For example, in Lisp the "square" function can be expressed as a lambda expression as follows:

This work also formed the basis for the denotational semantics of programming languages.

These formal systems are extensions of lambda calculus that are not in the lambda cube: