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)