lambda calculus

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It was developed by Alonzo Church in the 1930s as a way to investigate the fundamental nature of computation and computability.

A key feature of lambda calculus is its ability to represent functions. In this system, a function is defined by highlighting a variable, say x, in an expression, M, and understanding the result as a function of x. This function is expressed as ( \lambda x.M ), and it can be applied to other functions. The semantics for lambda calculus do not postulate individuals to which functions are applied; instead, everything is a function, and applying one function to another yields a function. This concept is closely related to the theory of programming languages and is fundamental to computer science.12