Lambda Calculus

Lambda Calculus is a theory of computable functions, i.e. a formal system which formalize the abstract notion of computable functions. This calculus was developed by Alonzo Church in the 1930s at the same time which other researchers developed other models of computation which later were proved to be equivalent. S. C. Kleene developed recursive functions and Alan M. Turing a Universal abstract machine, later called Universal Turing Machine, among other formal systems. Recursive functions can be expressed in the lambda calculus, and vice versa, also an universal Turing machine can be defined in the lambda calculus and recursive functions and the lambda calculus in the universal Turing machine, the same with the other computation models not described here. The fact that every attempt to build a system to capture the notion of computation resulted in a theory equivalent to each other is a strong indication that no other "more powerful" system exists, that can not be proved, for that reason is known as the Churrch-Turing thesis. In other words it states that any compuable function is definable indistinctly in any of those systems. You may noticed that formal system, theory and model are used to refer to those formalisms, lets say what that means. A formal theory is a formal system which captures the notion of the abstract notion of computable functions.

The lambda calculus is one foundation for computer science, like infinitesimal calculus is a foundation for the Newtonian physics. Another foundation is the Von Neumann machine, which is a hardware realization of a Universal Turing Machine, of course as any physical implementation it has finite memory.

The lambda calculus served as the basis for functional programming languages in the same way that the von Neumann machine is the basis for the imperative programming languages.

An important subject in computer science the semantics of programming languages, i.e. how to state the meaning of a programming language. The lambda calculus is the basis for a denotational semantics, developed by Dana Scott.

There are different lambda theories studied in the lambda calculus. The untyped lambda calculus resulted in an inconsistent theory because there is a paradox equivalent to the Russell paradox in the naive set theory. that motivated the development of typed lambda theories.

The untyped lambda calculus formulas are induced from an infinite set of variables, $x,y,z,\ldots ,x_{0},y_{0},z_{0},\ldots$, abstractions with the form $\lambda v.M$ where $v$ is a variable and $M$ a formula of the lambda calculus also called lambda term, the last is called applications with the form $(MN)$ where $M$ and $N$ are also lambda terms and nothing else.

There are conversion rules, $\alpha ,\beta$ and $\eta$ defined as follows:

Contents

1. Syntax
2. Equivalent formulas