5.3 函数与映射：定义域、像、单射和双射
档案城送来一份用户与邮箱的关系表，瞭望塔要求用函数、单射和满射精确描述其中的约束。
一张用户—邮箱表可能允许多个用户共享邮箱，也可能要求邮箱唯一；还可能存在没有邮箱的用户。数学函数把这些约束拆成“每个输入是否有输出”“输出是否唯一”“不同输入能否碰到同一输出”。
函数是一类受约束的关系
函数：
f:A→B要求对每个 a∈A，存在唯一 b∈B 使 (a,b)∈f：
∀a∈A ∃!b∈B, f(a)=b因此普通数学函数同时要求：
- 全定义：定义域中的每个输入都有输出；
- 单值：一个输入不能对应两个不同输出。
关系可以一对多、多对一或遗漏输入；函数只能多对一或一对一，不能一对多，也不能漏掉声明定义域中的元素。
定义域、陪域和像
对 f:A→B：
A：定义域（domain）；B：陪域（codomain）；f(A)={f(a)|a∈A}：像（image）。
像一定是陪域的子集，但未必等于陪域。
f:ℤ→ℤ
f(n)=2n陪域是全部整数，像只有偶数。中文资料有时把“值域”分别用于 codomain 或 image，容易歧义；严谨写作应明确使用“陪域”和“像”。
同一个计算规则配不同陪域，满射性质可能变化：
f:ℤ→ℤ, f(n)=2n // 不是满射
g:ℤ→2ℤ, g(n)=2n // 是满射函数不只由公式决定，定义域和陪域也是身份的一部分。
单射、满射、双射
单射
不同输入不会得到同一输出：
f(a₁)=f(a₂) → a₁=a₂等价地：a₁≠a₂ → f(a₁)≠f(a₂)。
满射
陪域中每个元素都被命中：
∀b∈B ∃a∈A, f(a)=b双射
同时单射和满射，每个陪域元素恰好有一个原像。双射建立一一对应，可用来证明集合等势。
例：
f:ℤ→ℤ, f(n)=n+1既单射又满射，逆函数 f⁻¹(n)=n-1。
左逆、右逆与真正的逆函数
若 g:B→A：
g∘f=id_A // g 是 f 的左逆，推出 f 单射
f∘g=id_B // g 是 f 的右逆，推出 f 满射当两式都成立时，f 双射，g 是唯一逆函数。
非单射函数不能从输出唯一恢复原输入；非满射函数若坚持在整个陪域定义逆，会遇到没有原像的元素。
编码/解码 API 应说明在哪个有效子域互逆，以及规范化是否丢失信息。
函数复合
f:A→B
g:B→C
g∘f:A→C
(g∘f)(a)=g(f(a))复合满足结合律：
h∘(g∘f)=(h∘g)∘f一般不满足交换律。类型边界还必须匹配：f 的陪域要适合作为 g 的定义域。
若 f,g 都单射，复合单射；若都满射，复合满射；若都双射，复合双射，且：
(g∘f)⁻¹=f⁻¹∘g⁻¹偏函数与全函数化
数学偏函数可能对某些输入没有定义：
reciprocal(x)=1/x，x≠0可以缩小定义域：
reciprocal:ℝ\{0}→ℝ也可以扩展陪域，把失败显式变成值：
safeReciprocal:ℝ→Option<ℝ>程序中的异常、崩溃和不终止都使“函数对所有输入返回一个声明类型的值”变得不成立。静态类型签名通常没有表达全部效应。
把预期失败建模成 Option/Result 能让调用方在普通控制流中处理；但资源耗尽、进程终止等仍可能位于模型之外。
数据库唯一键的准确类比
若把每一行映射到唯一键，且所有行都有非空键，唯一约束使这个映射对当前行集合是单射。但 SQL 中 NULL 的唯一约束语义因数据库而异，复合索引、条件索引也会改变适用范围。
唯一索引不保证满射：可能的键空间里绝大多数值没有对应行。主键还承担非空和行身份等数据库契约，不能只用“单射”概括。
加密函数并非一概双射
固定密钥的理想分组密码在固定长度块空间上表现为置换，因此加密和解密互逆。但现代加密方案通常还输入 nonce、随机数、关联数据，并产生带认证标签的密文；若只写成“明文→密文”，不同随机输入可产生不同密文。
所以“加密函数是双射”只在明确固定密钥、参数和有限块空间等模型下成立。安全性也不由双射性质单独保证。
有限集合上的函数计数
若：
|A|=m, |B|=n从 A 到 B 的函数共有：
n^m因为每个 A 元素独立选择 n 个输出之一。
当 m≤n，单射数量：
n(n-1)...(n-m+1)=n!/(n-m)!若 m>n，不存在单射，这就是抽屉原理的一种形式。第 6 章组合数学会继续使用。
API 设计检查
看到 UserId→Email 时，先问：
- 每个用户都有邮箱吗，还是偏函数？
- 多个用户可共享邮箱吗，是否单射？
- 陪域是所有合法邮箱字符串，还是已验证地址？
- 大小写和 Unicode 规范化怎样影响相等？
- 查询失败、超时和权限不足怎样进入结果类型？
- 映射随时间变化时，函数是否还需要时间参数？
数学记号能揭示缺失条件，但真实系统常需要把上下文和效应加入模型。
完成检查
对以下函数判断单射、满射和双射，并写出定义域、陪域和像：
f:ℤ→ℤ, f(n)=2n；g:ℝ→[0,∞), g(x)=x²；h:[0,∞)→[0,∞), h(x)=x²；k:ℤ→{0,1,2}, k(n)=n mod 3。
再把一个可能失败的配置解析函数改写成总函数结果类型，并说明哪些外部故障仍未被模型覆盖。