> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/340-lambda-calculi/lambda-calculus/lambda-functions.md).

# Functions in lambda calculus

A function is a special kind of relation that relates the source set (domain) to the target set (codomain).

Being a relation, a function is a set comprised of ordered pairs. The first component of a pair comes from the domain set, while the second component comes from the codomain set.

A function associates each element in a domain set to exactly one element in a codomain. This constraint is exactly what promotes a relation to the status of a function. A function is a *left-unique, right serial relation*.

In fact, there are two restrictions here: 1) all elements of a domain must be associated 2) each to exactly one element of a codomain.

Since, not all codomain elements may be included in an association, those that are form a subset of a codomain called range. And because of that, a function's definition must mention both domain and codomain, although the domain set may be derived from the function set itself - it is the set formed by taking all the first components of all the ordered pairs.

In math, a function has two "faces": a function definition and function application. First, a function needs to be defined and in mathematical notation this looks like `f(x) = x + 1`. A function definition is also called function abstraction. The other face is function application, e.g. `f(3)`, where the previously defined function bound to a variable (identifier) `f` is applied to an argument, `3` in this case.