The lambda calculus is: a simple programming language; a model of computation (akin to Turing machines and recursive functions), through which we can study the computability and complexity of functions and predicates; and an internal language for cartesian closed categories (for more on this see at relation between type theory and category theory). It comes in both typed and untyped versions. The basic constructs of lambda calculus are lambda abstractions and applications. If is an expression of some sort involving a free variable (possibly vacuously), then the lambda abstraction is intended to represent the function which takes one input and returns the result of substituting that input for in . Thus, for instance, is the function which adds one to its argument. Lambda expressions are often convenient, even outside lambda calculus proper, for referring to a function without giving it a name. Application is how we “undo” abstraction, by applying a function to an argument. The application of the function to the argument is generally denoted simply by . Applications can be parenthesized, so for instance and and all denote the same thing as . Application is generally considered to associate to the left. Thus denotes the application of to , followed by application of the result (assumed to again be a function) to . This allows the representation of functions of multiple variables in terms of functions of one variable via “currying” (named for Haskell Curry, although it was invented by Moses Schönfinkel): after being applied to the first argument, we return a function which, applied to the next argument, returns a function which, when applied to the next argument, … , returns a value. For instance, the “addition” function of two variables can be denoted : when applied to an argument , it returns a function which, when applied to an argument , returns . This is so common that it is generally abbreviated . Evaluation or reduction is the process of “computing” the “value”...