Lambda calculus

In mathematical logic and computer science, lambda calculus, also λ-calculus, is a formal system (a system that can be used to figure out different logical theories and ideas). It was made to explore different ways of creating and using mathematical functions, and it lays out rules for doing this. It is also a tool for exploring recursion, and it has been used to explain what a computable function is. It was made by Alonzo Church and Stephen Cole Kleene in the 1930s. In 1936, Church used lambda calculus to show that there is no solution to the Entscheidungsproblem.

Lambda calculus can be called the smallest universal programming language. At its core, lambda calculus is made up of just one transformation rule (something called variable substitution) and just one way to define a function. Each function definition has a list of the function's parameters, which are all of the variables that can be used in that function. Variable substitution is where specific variables in a function are replaced by other values (for example, the value [math]\displaystyle{ 2 }[/math] could take the place of every spot in a function where the variable [math]\displaystyle{ x }[/math] appears). This is called a transformation rule because it can be used to transform lambda expressions by changing around their values.

Lambda calculus is considered "universal" because it can be used to both create and find the answer to any computable function. This is exactly what a Turing machine can do, so lambda calculus and Turing machines are said to be equivalent. However, lambda calculus focuses more on the use of transformation rules. It does not care about the actual machine that puts those rules into place. It is an approach more related to software than to hardware.

There is no way to answer the question of whether two lambda calculus expressions are the same as each other (in more specific words, there is no general algorithm that can show that two lambda expressions are equivalent). This was the first problem where the idea of undecidability could be proven. Later, undecidability was also proven for the halting problem, where it was shown that there is no general way to show whether or not a program will keep running forever. Lambda calculus has had large effects on lots of functional programming languages, such as LISP, ML, and Haskell.