Page "Lambda calculus" Paragraph 0

Lambda calculus ( also written as λ-calculus or called " the lambda calculus ") is a formal system in mathematical logic for expressing computation by way of variable binding and substitution.

It was first formulated by Alonzo Church as a way to formalize mathematics through the notion of functions, in contrast to the field of set theory.

Although not very successful in that respect, the lambda calculus found early successes in the area of computability theory, such as a negative answer to Hilbert's Entscheidungsproblem.