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 [3vl $f : X \to Y$] (and say "$f$ has the [type_mathematics 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.

[fixme: Talk about how they're a pretty dang fundamental concept.] [fixme: Talk about how we can think of functions as mechanisms.] [fixme: Add pages on set theoretic and type theoretic formalizations.] [fixme: Talk about their relationships to programming.] [fixme: Talk about generalizations including partial functions, multifunctions, etc.] [fixme: 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)