环球报道:集合的形式化 #5 函数 (1)

(资料图片仅供参考)

在 Coq 中，我们通常称类型为 A -> B 的对象为“函数”，但这与数学上的“函数”有一定的区别。数学上的函数具有“定义域”的属性，从而有  。为了实现这种效果，我们可以用类型为 A -> option B 的对象来模拟数学上的 A -> B 函数。option 具有类型 Type -> Type，对于类型 A，具有类型 option A 的对象或者是 None，或者是 Some a（其中 a : A）。我们首先进行以下的准备工作：（注：下文中，“函数”可能指的是有定义域的数学上的函数，也可能指的是 A -> B 类型的对象，需要结合上下文判断）

IsSome 用于判断一个 option A 类型的对象是否可写成 Some a（其中 a : A）。x [∈] S 表示 x 可写成 Some a 且 a ∈ S。例如，IsSome (@None nat) = False，Some 0 [∈] {0,1,2}。opaque 用于将一个对象“不透明化”。例如，opaque 0 : nat，opaque 0 = opaque 1 = opaque 2 = ...，但我们无法证明 opaque 0 等于某一个具体的自然数形式（即 "0", "1", "2" 这种自然数的标准形式），也无法证明 opaque 0 不等于某一个具体的自然数形式。

用 A -> option B 类型的对象模拟函数也有其问题。例如，设 f : nat -> option nat，则 f 0 < f 1 是不符合语法的，因为“<”两边的必须都具有类型 nat。为了处理此类问题，我们可以定义一些函数来实现 A -> B、A -> option B、option A -> option B 类型的转换。

对于 f : A -> option B，# f # : option A -> option B，# f # (Some a) = f a，# f # None = None。对于 f : A -> B，[ f ] : A -> option B，[ f ] a = Some (f a)。对于 f : A -> option B 和 b : B，f_app f b : A -> B，若 f a = Some x，则 f_app f b a = x，若 f a = None，则 f_app f b a = opaque b。

现在，我们可以定义函数的定义域（dom）、值域（ran）、像（f_map）、逆像（f_imap）。

我们常用“单射”“满射”“双射”等词描述函数的性质，但它们的语法结构不尽相同：“单射”是一元谓词，是函数本身的属性；而“满射”“双射”都是三元谓词，是针对一个函数和两个集合而言的（因此“某函数是满射的”是不合理的表述，除非上下文已明确针对的集合）。它们的定义与基本定理如下：

对于集合 S 和 T，我们定义“函数空间 S T”（在数学上通常记为  或 ）为所有【定义域为 S，值域是 T 的子集】的函数组成的集合。对于函数 f : A -> option B，f 的函数图像是所有满足 f x = Some y 的 (x,y) 组成的集合。

关键词： SOME NONE 无法证明 OPAQUE