-Abstraction is the process of interpreting a formula for a function (or operation) as defining an actual function.
If in a context with a free variable of type we have a term of type , then
is a term (in a context without the free variable) of the dependent product type . If is defined in the context without the free variable, then this expression is a term of the function type or .
Often we make the presence of the free variable explicit in the notation, saying that is a term of type ; then
a term of the dependent product . Or if is a term of the constant type , then the same expression is a term of the function type .
Although developed for type theory and commonly used in computer science, -abstraction makes sense in ordinary mathematics usually based on set theory. If the types and are interpreted as sets and we define functions as certain subsets of cartesian products, then the notation (2) refers to
(at least in the simple case where is constant).
Created on June 15, 2012 at 00:18:39. See the history of this page for a list of all contributions to it.