|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|classical type theory?||internal logic||classical type theory?, logic programming?|
|cut elimination?||counit||beta reduction|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
The lambda calculus is:
a simple programming language;
It comes in both typed and untyped (or, more correctly, single-typed) 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
\lambda x. t
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” of a lambda term. The most basic operation is called beta reduction and consists in taking a lambda abstraction at its word about what it is supposed to do when applied to an input. For instance, the application reduces to (and thereby, presuming appropriate rules for , to ). Terms which can be connected by a zigzag of beta reductions (in either direction) are said to be beta-equivalent.
Another basic operation often assumed in the lambda calculus is eta reduction/expansion, which consists of identifying a function, with the lambda abstraction which does nothing other than apply to its argument. (It is called “reduction” or “expansion” depending on which “direction” it goes in, from to or vice versa.)
A more basic operation than either of these, which is often not even mentioned at all, is alpha equivalence; this consists of the renaming of bound variables, e.g. .
More complicated systems that build on the lambda calculus, such as various type theories, will often have other rules of evaluation as well.
In good situations, lambda-calculus reduction is confluent and terminating (the Church-Rosser theorem?), so that every term has a normal form?, and two terms are equivalent precisely when they have the same normal form.
In the pure “untyped” lambda calculus, there is only one kind of variable and one kind of term, and the only construction used to form expressions is application of a function to an argument , generally denoted simply . In particular, all variables and terms “represent functions”, and can be applied to any other variable or term.
From the point of view of type theory, it is more appropriate to call this “single-typed” or “unityped” lambda-calculus rather than “untyped” — there is a single type which all terms belong to.
As an example of the sort of freedom this allows, any term can always be applied to itself. We can then form the term which applies its argument to itself. The self-application of this term:
(\lambda x. x x) (\lambda x. x x)
is a classic example of a term which admits an infinite sequence of beta-reductions (each of which leads back to itself).
In pure untyped lambda calculus, we can define natural numbers using the Church numerals?: the number is represented by the operation of -fold iteration. Thus for instance we have , the function which takes a function as input and returns a function that applies twice. Similarly is the identity on functions, while takes any function to the identity function (the 0th iterate of ). We can then construct (very inefficiently) all of arithmetic, and prove that the arithmetic functions expressible by lambda terms are exactly the same as those computable by Turing machines or (total) recursive functions.
The most natural sort of model of pure lambda calculus is a set or other object which is equivalent to its own exponential . Of course there are no nontrivial such models in sets, but they do exist in other categories, such as domains. It is worth remarking that a necessary condition on such is that every term have a fixed-point; see fixed-point combinator.
In simply typed lambda calculus, each variable and term has a type, and we can only form the application if is of some type while is of a function type whose domain is ; the type of is then . Similarly, if is a variable of type and is a term of type involving , then has type .
Without some further type and term constructors, there is not much that can be done, but if we add a natural numbers object (that is, a type with constants of type and of type , along with a “definition-by-recursion” operator), then we can express many recursive functions. (We cannot by this means express all computable functions, although we can go beyond primitive recursive function?s; for instance we can define the Ackermann function?. One way to increase the expressiveness to all partial recursive functions is to add a fixpoint? combinator?, or an unbounded search operator).
Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while
Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.
These two operations are adjoint in an appropriate sense.