Intuitively, a function \(f\) 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 \(f\) is a relationship between a set \(X\) of inputs and a set \(Y\) of outputs, which relates each input to exactly one output. For example, \(-\) is a function that relates the pair \((4, 3)\) to \(1,\) and \((19, 2)\) to \(17,\) and so on. In this case, the input set is all possible pairs of numbers, and the output set is numbers. We write \(f : X \to Y\) (and say “$f$ has the type \(X\) to \(Y\)”) to denote that \(f\) is some function that relates inputs from the set \(X\) to outputs from the set \(Y\). For example, \(- : (\mathbb N \times \mathbb N) \to \mathbb N,\) which is read “subtraction is a function from natural number-pairs to natural numbers.”

\(X\) is called the domain of \(f.\) \(Y\) is called the codomain of \(f\). 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.

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 \(f : \mathbb{R} \to \mathbb{R}\) from the real numbers to the real numbers which sends every real number to its square; symbolically, we can write \(f(x) = x^2\).

(TODO)