部分函数

部分函数把“输入没有对应输出”纳入定义本身，而不是额外发明一个普通值，适合描述尚未终止、前置条件不满足或搜索失败的程序，只接受部分输入的解析器，以及未必存在的代数运算。它与返回 null 的全函数不同：null 仍是陪域中的一个值，而部分函数在该点根本没有函数值。把定义域显式写成 $D\subseteq X$，可以分离“计算结果是什么”和“哪些输入上有结果”两个问题。

实数上的 $x\mapsto 1/x$ 可视为 $\mathbb{R}\rightharpoonup \mathbb{R}$，定义域为 $\mathbb{R}\setminus \{0\}$；数组查找也可建模为从键到元素的部分函数。把未定义统一编码为 $\mathrm{\perp }$ 可得到 $A\to B\cup \{\mathrm{\perp }\}$，但只有在 $\mathrm{\perp }$ 不与合法输出混淆并保留相应语义时才等价。

列表取首元素函数 $\mathrm{head}$ 只在非空列表上有值：$\mathrm{head}([a_1,\dots ,a_n])=a_1$，但 $\mathrm{head}([])$ 未定义。若把返回类型改为 option 并令空列表返回 None，就得到一个不同的全函数；这说明“未定义”与“返回失败值”是两种建模选择。

部分函数仍要求每个定义域内输入最多对应一个输出；一个输入可产生两个或更多合法结果的是关系或多值函数，不能仅靠“部分”二字表达。把未定义点随意补成默认值会改变等式、复合与可计算性问题，必须明确这种全化选择。

函数公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。 的通常定义可视为定义域等于整个源集合的特例，部分函数则常与 关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。 区分使用，并由此连接函数论、可计算性与程序语义。在可计算性中，部分可计算函数公理库部分可计算函数Partial computable function允许机器在函数未定义的输入上不停机的部分函数。 用不终止或“发散”表示未定义，连接到可识别语言；偏代数用它表达只在满足前提时存在的运算，数据库与 API 规范也借它区分缺失、失败和正常值，而程序语义可用它刻画可能发散的程序含义。