函数

函数可以想成一份输入—输出契约，但不必是一段可执行程序。契约先规定哪些输入合法，再为每个合法输入指定唯一结果。公式、表格、几何构造和存在性定理，都可能用来指定这种对应。

例如“给每个人指定其出生日期”在信息完整且约定明确时可以建模为函数；多个人同日出生没有问题。“给每个人列出所有朋友”也能成为函数，只要输出类型是“人的集合”；若输出类型仍是“一个人”，则需要另加挑选规则。是否单值，要连同输出对象的类型一起判断。

$\mathbb{R}\to \mathbb{R}$ 的 $x\mapsto x^2$ 与 $\mathbb{R}\to [0,\mathrm{\infty })$ 的同一公式具有相同函数图，但陪域不同：前者不是满射，后者是满射。是否覆盖所有声明的输出，不可能只由公式的字面形状决定。

一个平方函数，三种操作 ​

取 $f:\mathbb{R}\to \mathbb{R}$，$f(x)=x^2$。求单点值有 $f(-2)=4$；求像有 $f[[-2,1]]=[0,4]$；求逆像则有

逆像包含两个区间，仍然是唯一确定的集合。与此不同，“$4$ 的逆函数值”在这个函数上没有定义，因为 $-2$ 与 $2$ 都映到 $4$。把定义域限制为 $[0,\mathrm{\infty })$，并把陪域也取为 $[0,\mathrm{\infty })$，才得到具有逆函数 $y\mapsto \sqrt{y}$ 的新函数。

像与逆像的集合运算也不同。逆像保留交集，因为

像通常只有 $f[S\cap T]\subseteq f[S]\cap f[T]$。仍用平方函数，令 $S=\{-1\}$、$T=\{1\}$：输入集合不交，但两个像都为 $\{1\}$。不同输入被合并，正是反向包含失败的原因。像保留并集；若函数是单射，像也保留两个子集的交集。逆像则对任意函数都保留并、交与补，其中补集分别相对于定义域和陪域：$f^{-1}[B\setminus T]=A\setminus f^{-1}[T]$。这使它成为连续性和可测性定义中的基本操作。

“每个输入有且仅有一个输出”的边界 ​

关系 $\{(1,a),(1,b)\}$ 在 $a\ne b$ 时不是函数图，因为输入 $1$ 对应两个结果。关系 $\{(1,a)\}$ 也不是从 $\{1,2\}$ 到 $\{a\}$ 的函数图，因为遗漏了输入 $2$。这分别违反唯一性和全定义性。

若允许源集合中部分输入没有值，就得到部分函数理路部分函数Partial function在声明的源集合的一部分上赋值，实际定义域由已有函数值的输入组成。；通常的函数是它处处有定义的特例。把未定义编码为一个新的失败值，可以改造成全函数，但必须扩大陪域，并明确这个值不与合法结果混淆。

空定义域同样满足定义：对每个 $B$，恰有一个函数 $\varnothing \to B$，其图为空。若定义域非空、陪域为空，则没有函数。这里“对所有输入”在没有输入时自动成立；一旦有输入，存在输出的要求就无法满足。

复合与逆函数 ​

给定 $f:A\to B$ 和 $g:B\to C$，复合函数理路函数复合Function composition · Composition of maps按先 f 后 g 的次序把映射串联为 g∘f。定义为 $(g\circ f)(a)=g(f(a))$。中间集合 $B$ 保证前一步输出是后一步合法输入。对 $h:C\to D$，两种加括号方式在每个 $a$ 上都得到 $h(g(f(a)))$，所以复合满足结合律。

恒等映射满足 $f\circ {\mathrm{id}}_A=f$ 与 ${\mathrm{id}}_B\circ f=f$。这里采用源、目标匹配的带类型复合；若实际像只落在下一函数的定义域内，而声明的陪域不匹配，应先说明对陪域或定义域的调整。限制 $f{|}_S:S\to B$ 缩小输入范围；把陪域收缩到 $f[A]$ 则保留函数图，并得到满射。

若 $f(a)=f(a^{\prime })$ 只能在 $a=a^{\prime }$ 时成立，称 $f$ 为单射理路单射Injective function · One-to-one function不同输入必有不同输出的函数。；若 $f[A]=B$，称它为满射理路满射Surjective function · Onto function陪域中每个元素都有至少一个原像的函数。。同时满足两者便是双射理路双射Bijective function · One-to-one correspondence让每个陪域元素恰有一个原像、等价于存在唯一双侧逆函数的映射。，此时每个 $b\in B$ 恰有一个原像，因而能定义唯一的逆函数，并满足

只给出一个方向的逆等式，保证也相应减弱：存在左逆会推出单射，存在右逆会推出满射。双射把两侧的存在性与唯一性同时配齐。

同一种接口，不同的数学结构 ​

序列理路序列Sequence以自然数为定义域的函数。把输入取为自然数索引；概率论中的随机变量把输入取为随机结果，并要求逆像可测；连续函数则要求开集的逆像仍为开集。后两种性质都不是函数定义自带的，而是对既有对应额外提出的要求。

数学函数也不自动具有算法。计算一个函数意味着给出在所声明输入上产生正确输出的有效过程；读取时钟或随机数的程序，只有将这些影响输出的因素纳入输入模型后，才适合描述为确定函数。函数的存在、公式是否容易求值、程序是否终止，是不同层次的问题。把类型、对应与实现分开，才能准确讨论数学定义和程序接口。