λ\lambda-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 xx of type AA we have a term tt of type BB, then

(1)λ x:At \lambda_{x\colon A} t

is a term (in a context without the free variable) of the dependent product type x:AB\prod_{x\colon A} B. If BB is defined in the context without the free variable, then this expression is a term of the function type ABA \to B or B AB^A.

Often we make the presence of the free variable explicit in the notation, saying that t[x]t[x] is a term of type B[x]B[x]; then

(2)λ x:At[x], \lambda_{x\colon A} t[x] ,

a term of the dependent product x:AB[x]\prod_{x\colon A} B[x]. Or if t[x]t[x] is a term of the constant type BB, then the same expression is a term of the function type ABA \to B.

In set theory

Although developed for type theory and commonly used in computer science, λ\lambda-abstraction makes sense in ordinary mathematics usually based on set theory. If the types AA and BB are interpreted as sets and we define functions as certain subsets of cartesian products, then the notation (2) refers to

{(x,y)A×By=t[x]} \{ (x,y) \in A \times B \;|\; y = t[x] \}

(at least in the simple case where BB is constant).

Created on June 15, 2012 00:19:56 by Toby Bartels (