Function

Written by Nate Soares, et al. last updated

Intuitively, a function is a procedure (or machine) that takes an input and performs some operations to produce an output. For example, the function "+" takes a pair of numbers as input and produces their sum as output: on input (3, 6) it produces 9 as output, on input (2, 18) it produces 20 as output, and so on.

Formally, in mathematics, a function is a relationship between a set of inputs and a set of outputs, which relates each input to exactly one output. For example, is a function that relates the pair to and to and so on. In this case, the input set is all possible pairs of numbers, and the output set is numbers. We write (and say " has the type to ") to denote that is some function that relates inputs from the set to outputs from the set . For example, which is read "subtraction is a function from natural number-pairs to natural numbers."

is called the domain of is called the codomain of . We can visualize a function as a mapping between domain and codomain that takes every element of the domain to exactly one element of the codomain, as in the image below.

Domain, Codomain, and Image

Talk about how they're a pretty dang fundamental concept.
Talk about how we can think of functions as mechanisms.
Add pages on set theoretic and type theoretic formalizations.
Talk about their relationships to programming.
Talk about generalizations including partial functions, multifunctions, etc.
Give some history, e.g. Church-Turing, Ackerman, recursion, etc. (Many of these todos should go into separate lenses; this definition here might be fine?)

Examples

There is a function from the real numbers to the real numbers which sends every real number to its square; symbolically, we can write .

(TODO)