Lambda calculus

In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what is a computable function. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

Computable functions and lambda calculus

A function F: N → N of natural numbers is a computable function if and only if there exists a lambda expression f such that for every pair of x, y in N,  F(x) = y  if and only if  f x == y,  where x and y are the Church numerals corresponding to x and y, respectively. This is one of the many ways to define computability; see the Church-Turing thesis for a discussion of other approaches and their equivalence.

Related Topics:
Natural number - Computable function - If and only if - Church-Turing thesis

~ ~ ~ ~ ~ ~ ~ ~ ~ ~