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.

Lambda calculus and programming languages

Most functional programming languages are equivalent to lambda calculus extended with constants and datatypes. Lisp uses a variant of lambda notation for defining functions, but only its purely functional subset is really equivalent to lambda calculus. Strictly speaking, this holds only for modern dialects of Lisp, such as Common Lisp and Scheme. More archaic Lisps, such as Emacs Lisp, still use dynamic binding, and so are not based on the lambda calculus. Rather, they are based on the syntax of the lambda calculus, together with a misunderstanding of the notion of binding and substitution in the lambda calculus. In Lisp terminology, this is known as the Funarg problem.

Related Topics:
Functional programming language - Constant - Datatype - Lisp - Common Lisp - Scheme - Emacs Lisp - Dynamic binding - Substitution - Funarg problem

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The lambda calculus is a fundamental in theoretical computer science and in programming language theory.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Theory of the lambda calculus says that lambda calculus computations can always be carried out sequentially not that they must be carried out sequentially. The lambda calculus is suitable for expressing some kinds of parallelism, e.g., the parallel evaluation of the arguments of a procedure. However the lambda calculus does not in general implement concurrency, e.g., a shared financial account that is updated concurrently. On the other hand concurrent computation as in the Actor model and Process calculi can perform the parallelism of the lambda calculus. The difference between parallelism in the lambda calculus and concurrency in Actors is reflected in that the Actor model has unbounded nondeterminism whereas the nondeterministic lambda calculus has bounded nondeterminism.

Related Topics:
Parallelism - Concurrency - Actor model - Process calculi - Unbounded nondeterminism

~ ~ ~ ~ ~ ~ ~ ~ ~ ~