从 Semantics 到 Category Theory

1. Motivation：从 error propagation 说起

比如在 denotational semantics 里，我们给程序一个数学上的 meaning：

⟦ 3 + 5 ⟧ = 8

但是：

3 \div 0

就会出现 error。因此，原本的结果空间 $ℚ_{\geq 0}$ 需要扩展成：

D = ℚ_{\geq 0} \cup {err}

然后每个 operation 都需要处理 error propagation。比如一个二元操作 $f$ ，需要扩展成：

\bar{f} (x, y) = {\begin{cases} f (x, y) & x \neq err, y \neq err \\ err & otherwise \end{cases}

对于除法，分母为 0 时， $f$ 本身也取 err。

这样写当然没错，但是会重复。加法这样写，乘法这样写，除法还是这样写。

这里真正重复的不是 operation，而是：如何给一个 computation space 加入 failure，以及之后的 maps 如何 preserve 这个 failure。

所以我们希望把这种 structure 单独抽出来，而不是每次重新写 case distinction。这也是 Category Theory 在这里出现的 motivation。

后面我们会看到，刚才的 err 可以先被重新理解成一个 base point，然后“给一个 set 加入一个 base point”这件事情本身还可以继续 generalize。

2. Category：Objects 和 Morphisms

一个 category $𝒞$ 里面有一类 objects。对于两个 objects $A$ 和 $B$ ，可以有从 $A$ 到 $B$ 的 morphisms：

f : A \to B

但是只有 objects 和 morphisms 还不够。Category 还要求这些 morphisms 具有两种基本 structure：identity 和 composition。

对于每一个 object $A$ ，都必须存在一个 identity morphism：

{id}_{A} : A \to A

它可以理解成“什么都不做”。另外，如果两个 morphisms 可以首尾连接：

f : A \to B, g : B \to C

那么它们可以 compose，得到：

g \circ f : A \to C

这里注意，先做的是 $f$ ，再做 $g$ 。Identity 和 composition 还必须满足两个基本规律。

Identity law：

{id}_{B} \circ f = f = f \circ {id}_{A}

Associativity（对于可组合的 $f, g, h$ ）：

h \circ (g \circ f) = (h \circ g) \circ f

所以更准确地说，一个 category 包含 objects、objects 之间的 morphisms，以及 morphisms 上定义的 identity 和 composition，并且满足上面两个规律。

Category Theory 关注的重点不是 object 内部有什么，而是 objects 之间有什么关系，以及这些关系怎样组合。下面看几个例子。

2.1 Example 1：Set

最熟悉的例子就是 Set。在 Set 里面：

sets 是 objects；
functions 是 morphisms。

例如 $f : X \to Y$ ，其中 $X$ 、 $Y$ 是两个 sets。Identity morphism 就是普通的 identity function：

{id}_{X} : X \to X, {id}_{X} (x) = x

Composition 也是普通的 function composition。如果 $f : X \to Y$ ， $g : Y \to Z$ ，那么 $g \circ f : X \to Z$ ，并且：

(g \circ f) (x) = g (f (x))

所以我们平时使用 sets 和 functions，其实已经是在一个 category 里面工作了。

2.2 Example 2：Set•

第二个例子和最开始的 err 就开始有关系了。Set• 是 based sets 的 category。它的 objects 是：

(X, x_{0})

其中 $x_{0} \in X$ 是一个 distinguished point，也就是 base point。而 morphism：

f : (X, x_{0}) \to (Y, y_{0})

不仅需要是一个 function，还必须 preserve base point：

f (x_{0}) = y_{0}

所以回头看前面的 $D = ℚ_{\geq 0} \cup {err}$ 。如果把 err 指定为 base point，那么：

(D, err)

其实就是一个 object in Set•。这样 err 就不再只是 semantics 定义里面临时添加的一个特殊 case，而成为了 object 本身携带的一部分 structure。

不过到这里，我们只是把 error 结构化了。至于能不能进一步把“给一个 set 添加 error”这件事情本身也统一起来，我们后面讲 functor 的时候再回来。

2.3 Example 3：Rel

再看 Rel。Rel 的 objects 仍然是 sets，但是 morphisms 不再是 functions，而是 relations。例如：

R : A \to B, R \subseteq A \times B

这里可以看出一个很重要的点：morphism 不一定是 function。在 Rel 里面，object $A$ 的 identity morphism 是：

{id}_{A} = {(a, a) ∣ a \in A}

如果 $R : A \to B$ ， $S : B \to C$ ，那么 composition 是：

S \circ R = {\begin{cases} (a, c) ∣ \exists b \in B : \\ (a, b) \in R \land (b, c) \in S \end{cases}}

所以 Rel 同样有 identity 和 composition，并且满足 identity law 和 associativity。Category 真正在意的不是 morphism 到底是不是 function，而是这些 morphisms 能不能 compose，以及 composition 是否 obey category laws。

2.4 Set 和 Rel 的区别

Set 和 Rel 的 objects 都是 sets，但它们不是同一个 category。真正不同的是 morphisms。

Set：

objects = sets；
morphisms = functions $f : A \to B$ ；
每个 $a \in A$ 必须对应唯一一个 $b \in B$ 。

Rel：

objects = sets；
morphisms = relations $R \subseteq A \times B$ ；
一个 $a$ 可以对应 0 个、1 个或者多个 $b$ 。

函数其实只是 relation 的一种特殊情况。

所以 object 一样，不代表 category 一样；还要看 morphisms、identity 和 composition 是怎样定义的。

3. Diagram 和 Commutativity

当然，我们是视觉动物。Category Theory 里面经常直接用 diagram 表示 objects 和 morphisms。

g \circ f = h \circ {id}_{A}

如果从同一个 object 出发，到同一个 object 结束，不同 path 对应的 composed morphisms 相等，我们就说这个 diagram commutes。

也就是：different paths, same result.

因为 $h \circ {id}_{A} = h$ ，所以这里其实也可以写成：

g \circ f = h

4. Isomorphism

如果有 $f : A \to B$ ，并且存在 $g : B \to A$ ，满足：

g \circ f = {id}_{A}, f \circ g = {id}_{B}

那么 $f$ 是一个 isomorphism， $g$ 是它的 inverse。写成：

A ≅ B

意思不是 $A$ 和 $B$ literally equal，而是它们在当前 category 关心的 structure 下可以互相转换，并且不丢信息。在 Set 里面，isomorphism 就是 bijection。

5. 再抽象一次：Functor

有了 category 之后，自然可以继续问：category 和 category 之间的 structure 怎样对应？这里就需要引入 functor：

F : 𝒞 \to 𝒟

因为一个 category 本身有 objects 和 morphisms，所以 functor 需要同时处理这两部分。

对于 object：

A \mapsto F (A)

对于 morphism $f : A \to B$ ，变成：

F (f) : F (A) \to F (B)

但是 functor 不能乱 mapping。它必须 preserve category 最重要的两种 structure：identity 和 composition。

F ({id}_{A}) = {id}_{F (A)}

F (g \circ f) = F (g) \circ F (f)

所以 functor 本质上就是：structure-preserving mapping between categories.

也可以理解成，它会 preserve commutative diagrams。如果原来 $g \circ f = h$ ，那么：

F (g) \circ F (f) = F (h)

所以原本 commute 的 diagram，经过 functor 之后仍然 commute。

Category 里面有 morphisms。Category 和 Category 之间有 functors。

5.1 Functor Example 1：Forgetful Functor

一个很直观的例子是：

U : {𝐒𝐞𝐭}_{•} \to 𝐒𝐞𝐭

对于一个 based set $(X, x_{0})$ ，定义：

U (X, x_{0}) = X

也就是说，把 base point 这层额外的 structure 忘掉。对于一个 based map：

f : (X, x_{0}) \to (Y, y_{0})

定义：

U (f) = f

function 本身没有变化，只是不再关心它 preserve base point 这件事。所以 $U$ 被称为 forgetful functor。

5.2 Functor Example 2：Graph Functor

给定一个函数 $f : X \to Y$ ，可以定义它的 graph：

Gr (f) = {(x, y) \in X \times Y ∣ f (x) = y}

一个 function 可以看成一个特殊的 relation。这就把 Set 里的 morphism 送到了 Rel 里，给出一个 functor：

Gr : 𝐒𝐞𝐭 \to 𝐑𝐞𝐥

在 objects 上保留原来的 set；在 morphisms 上，把函数送到它的 graph：

Gr (X) = X, f \mapsto Gr (f)

Identity function 的 graph 正好是 identity relation；先复合函数再取 graph，也等于先取 graph 再做 relation composition：

Gr ({id}_{X}) = {(x, x) ∣ x \in X}

Gr (g \circ f) = Gr (g) \circ Gr (f)

所以 identity 和 composition 都被 preserve，Gr 确实是一个 functor。

6. Lemma 2.9：给一个 Set 加上 base point

给 set X 加一个新 base point，得到 EX。这个 construction 是 functor，并让普通 map $f : X \to U ((Y, y_{0}))$ 唯一扩展成 based map $\bar{f} : E X \to (Y, y_{0})$ 。

怎么给 X 加一个 base point？

X ⊔ {*}

即在 X 外加入新点 ∗，也写作 $X + 1$ 。教材的具体实现是：

E X = ({0} \cup {(1, x) ∣ x \in X}, 0)

不能直接写 $X \cup {0}$ ，因为 0 可能已在 X 中。把 x 包装成 $(1, x)$ 后，新增的 0 就与原元素不同，指定它为 base point。

$i_{X} (x) = (1, x)$ 把 X 放进 EX；U 仍是 forgetful functor。

这个 proof 只有两件事：

证明 E 真的是一个 functor；
证明 f 的 based extension 存在且唯一。

Part 1：E 是 functor

对 $f : X \to Y$ ，定义：

\begin{array}{l} (E f) (1, x) = (1, f (x)) \\ (E f) (0) = 0 \end{array}

普通元素按 f 走，base point 仍送到 base point。

Identity： $E ({id}_{X}) = {id}_{E X}$ ，因为 $(1, x)$ 和 0 都被送回自身。

Composition：对 $f : X \to Y$ 、 $g : Y \to Z$ ，关键计算是：

(1, x) \overset{E f}{\to} (1, f (x)) \overset{E g}{\to} (1, g (f (x)))

而 base point 始终是 $0 \to 0 \to 0$ ，因此：

E (g \circ f) = E g \circ E f

所以 $E : 𝐒𝐞𝐭 \to {𝐒𝐞𝐭}_{•}$ 确实是一个 functor。

Part 2：extension 存在且唯一

给定 $f : X \to U ((Y, y_{0}))$ ，直接定义：

\begin{array}{l} \bar{f} (1, x) = f (x) \\ \bar{f} (0) = y_{0} \end{array}

原元素按 f 走，新 base point 送到目标的 base point。

存在 / diagram commute：

U (\bar{f}) (i_{X} (x)) = \bar{f} (1, x) = f (x)

所以 $U (\bar{f}) \circ i_{X} = f$ 。图中虚线就是这个 extension 的底层 map。

为什么是唯一的？设 based map $h : E X \to (Y, y_{0})$ 也满足 $U (h) \circ i_{X} = f$ 。EX 只有两种元素：

对于普通元素 $(1, x)$ ，由 diagram commute：

h (1, x) = f (x) = \bar{f} (1, x)

对于 base point 0，因为 h 是 based map：

h (0) = y_{0} = \bar{f} (0)

每个元素上的值都相同，所以 $h = \bar{f}$ 。普通元素的值由 commutative diagram 决定，base point 的值由 based-map 条件决定，没有自由度，因此 extension 唯一。

核心就是：X 加一个新 base point 得到 EX，普通 map 随之唯一扩展成 based map。前面的 err 就可以看成这个新点。

8. Context 和 Substitution

前面 Category、Functor 的工具已经有了，Lemma 2.9 也准备好了处理 error / base point 的 extension。但放回 program semantics 里面，还缺一个具体答案：program 本身怎么 composition？

如果 semantics 要成为一个 functor，syntax 这一边首先得有一个 category。连 program 的 composition 都还没有 formalise，就还谈不上让 semantics 去 preserve 它。

对于 Arith，这个 composition 就是把一个 expression 填进另一个 expression 预留的位置，也就是 substitution。所以先引入 context 和 hole，再证明 substitution 满足 associativity、hole 充当 identity，才能得到后面的 classifying category $𝒞_{Arith}$ 。

Definition 3.1 给出 Arith 的 context grammar：

c ::= - | c □ e | e □ c | c □ c

其中 $□ \in {\oplus, \otimes, ⊘}$ ， $-$ 叫作 hole，e 是普通 Arith expression。

Context 就是带 hole 的 expression，例如 $- \oplus 5$ 、 $3 ⊘ -$ 。这里真正重要的是：可以把另一个 context 或 expression 填进去；有多个 holes 时，就填入每一个。

$c′ [c]$ 表示把 c substitution 到 c′ 的 holes 里，递归定义是：

- [c] = c

(c_{1} □ e) [c] = c_{1} [c] □ e

(e □ c_{2}) [c] = e □ c_{2} [c]

(c_{1} □ c_{2}) [c] = c_{1} [c] □ c_{2} [c]

填入普通 expression e 时，写作 $c [e]$ 。Substitution 就是 program composition 在 syntax 层面的具体操作。

8.1 Example 3.2

c_{1} = - \oplus 5

c_{2} = 3 ⊘ -

那么：

c_{1} [c_{2}] [6] = ((3 ⊘ -) \oplus 5) [6]

c_{1} [c_{2}] [6] = (3 ⊘ 6) \oplus 5

所以一个 context 可以先塞进另一个 context，最后再把 expression 填进去。

8.2 Lemma 3.3

对任意 c₁、c₂、c₃：

c_{1} [c_{2} [c_{3}]] = c_{1} [c_{2}] [c_{3}]

c_{1} [-] = c_{1} = - [c_{1}]

先把 c₃ 填进 c₂ 再填进 c₁，与先填 c₂ 再填 c₃ 相同；hole 则不改变填入结果。

对 c₁ 做 structural induction：grammar 有 hole 和三种递归构造。

Base case：c₁ = −。Hole 直接返回填入内容：

- [c_{2} [c_{3}]] = c_{2} [c_{3}] = (- [c_{2}]) [c_{3}]

Induction hypothesis (IH)：下文 c₁、c₁′ 指更小的子-context，假设对任意 c₂、c₃：

\begin{array}{l} c_{1} [c_{2} [c_{3}]] = c_{1} [c_{2}] [c_{3}] \\ c_{1}^{'} [c_{2} [c_{3}]] = c_{1}^{'} [c_{2}] [c_{3}] \end{array}

Induction cases（□ 为运算符）：

Case 1： $c_{1} □ e$

\begin{array}{l} (c_{1} □ e) [c_{2} [c_{3}]] \\ = c_{1} [c_{2} [c_{3}]] □ e \\ = c_{1} [c_{2}] [c_{3}] □ e by IH \\ = (c_{1} [c_{2}] □ e) [c_{3}] \\ = (c_{1} □ e) [c_{2}] [c_{3}] \end{array}

按定义下推到子-context，用 IH，再按定义合回。

Case 2： $e □ c_{1}$ ，同理在右侧用 IH。

Case 3： $c_{1} □ c_{1}^{'}$ ，两侧各用 IH，再合回：

\begin{array}{l} c_{1} [c_{2} [c_{3}]] □ c_{1}^{'} [c_{2} [c_{3}]] \\ = c_{1} [c_{2}] [c_{3}] □ c_{1}^{'} [c_{2}] [c_{3}] \\ = (c_{1} □ c_{1}^{'}) [c_{2}] [c_{3}] \end{array}

四类齐全，结合律得证。单位律同样作结构归纳。

二者正是 category composition 所需的两条 laws。

9. Classifying Category

由 Lemma 3.3，可以构造 Arith 的 classifying category $𝒞_{Arith}$ 。它只有一个 object $*$ ：

𝒞_{Arith} (*, *) = {c ∣ c is a context}

Identity 和 composition 定义为：

{id}_{*} = -

c_{2} \circ c_{1} = c_{2} [c_{1}]

当前 Arith 是 untyped 的，所以所有 contexts 都作为 $c : * \to *$ 。Objects 是 $*$ ，morphisms 是 contexts，identity 是 hole，composition 是 substitution。

于是 Arith 的 syntax / program composition 本身被组织成了一个 category。

10. Functorial Semantics

10.1 Theorem 3.4

回到前面的 functor：denotational semantics of Arith 给出

S : 𝒞_{Arith} \to {𝐒𝐞𝐭}_{•}

S (*) = (D, err)

D 就是前面的 semantic domain。对于一个 context $c : * \to *$ ，我们需要一个 based map：

S c : (D, err) \to (D, err)

Sc 从哪里来？对普通输入 $a \in ℚ_{\geq 0}$ ，先定义 $f : ℚ_{\geq 0} \to D$ ：

f (a) = ℰ ⟦ c [a] ⟧

也就是把 a 填进 c，再取 denotational semantics。但 Sc 要定义在整个 D 上，因此用 Lemma 2.9 把 f 唯一 extend 成 based map：

S c : D \to D

(S c) (err) = err

i 是把正常值嵌入 D 的 inclusion。虚线 U(Sc) 是 extension 的底层 map，使两条 path 相同。前面 Lemma 2.9 里“加一个 base point，再把普通 map 唯一 extend 成 based map”的结构，这里真的用上了。

Identity law 是：

S ({id}_{*}) = {id}_{S (*)}

因为 ${id}_{*} = -$ ，所以 $S (-) = id$ ：hole 什么都不做，semantic map 也什么都不做。

更重要的是 composition：

S (c_{2} \circ c_{1}) = S (c_{2}) \circ S (c_{1})

在 $𝒞_{Arith}$ 中，composition 就是 substitution，因此：

S (c_{2} [c_{1}]) = S (c_{2}) \circ S (c_{1})

左边先在 syntax 中 substitution，再求整体 semantics；右边先求每个 context 的 semantic map，再 compose 这些 maps。Functor law 要求两种方式相同。

也就是说，semantics 不只是给每个 program 一个 meaning，它还要 preserve program 本来的 composition structure。

这里只作 illustration。取： $c_{1} = - \oplus 5$ $c_{2} = 3 \otimes -$ $c_{2} [c_{1}] = 3 \otimes (- \oplus 5)$ 输入 2，先 substitution 再求 semantics，得到 $3 \times (2 + 5) = 21$ 。分开计算则是： $S (c_{1}) (2) = 7$ $S (c_{2}) (7) = 21$ 所以： $S (c_{2} [c_{1}]) (2) = (S (c_{2}) \circ S (c_{1})) (2)$

10.2 Example 3.5

Operational semantics 也给出一个 functor：

O : 𝒞_{Arith} \to {𝐒𝐞𝐭}_{•}

O (*) = (𝒫 (ℚ_{\geq 0}), \emptyset)

这里 𝒫 是 power set。对 context c 和 $U \subseteq ℚ_{\geq 0}$ ，定义：

(O c) (U) = {b \in ℚ_{\geq 0} ∣ \exists a \in U : c [a] ⇓ b}

也就是存在某个输入 a ∈ U，使得 c[a] ⇓ b。O 收集通过 operational semantics 能得到的正常结果，而不只取一个 number。

(O c) (\emptyset) = \emptyset

所以 Oc 是 based map。Hole 对应 identity，context substitution 对应这些 maps 的 composition：

O (-) = id

O (c_{2} [c_{1}]) = O (c_{2}) \circ O (c_{1})

因此 O 也 preserve identity 和 composition。现在有了两个 semantics functors：它们都解释同一个 syntax，彼此之间怎么正式建立关系？

11. Natural Transformation

一个 functor 可以看成一种 semantics / model。现在有 $S, O : 𝒞_{Arith} \to {𝐒𝐞𝐭}_{•}$ ，要比较的是这两种 semantics。

更一般地， $F, G : 𝒞 \to 𝒟$ 是两个 parallel functors，即 domain 和 codomain 相同。Natural transformation 就是用来比较它们的 structure。

Objects 之间有 morphisms；categories 之间有 functors；parallel functors 之间有 natural transformations。

11.1 Definition 3.6

若 $F, G : 𝒞 \to 𝒟$ ，一个 natural transformation：

α : F \Rightarrow G

由每个 object A ∈ 𝒞 对应的 morphism 组成：

α_{A} : F (A) \to G (A)

这些 components 必须满足 naturality condition。对任意 $f : A \to B$ ，下面的 square 要 commute：

G (f) \circ α_{A} = α_{B} \circ F (f)

两条 path 相同：先通过 F(f)，再用 α_B；或者先用 α_A 转到 G，再通过 G(f)。每个 object 上单独有一个 map 不够，这些 maps 还必须和所有 morphisms compatible。

$α_{A}$ 对每个 A 单独合法还不够，整个 family ${α_{A}}$ 必须 uniform / structure-compatible。这里真正限制的是：不同 object 上的 maps 不能各自随便做选择，而要和原 category 中所有 morphisms 一起 commute。

顺手记下 Exercise 3.3 / 3.4 的两个事实。若 $F : 𝒞 \to 𝒟$ 、 $G : 𝒟 \to ℰ$ ，就有 functor： $G \circ F : 𝒞 \to ℰ$ $(G \circ F) (X) = G (F (X))$ $(G \circ F) (f) = G (F (f))$ 每个 category 𝒞 也有 identity functor ${Id}_{𝒞} : 𝒞 \to 𝒞$ ，它在 objects 和 morphisms 上都什么也不改变。

Exercise 3.5 指出，Lemma 2.9 中的 $i_{X} : X \to U (E X)$ 当 X 变化时，形成一个 natural transformation： $i : {Id}_{𝐒𝐞𝐭} \Rightarrow U \circ E$ 对任意 $f : X \to Y$ ，满足： $U (E f) \circ i_{X} = i_{Y} \circ f$ 之前是一个 X 一个 X 地看 inclusion；现在可以看到，这些 inclusions 本身也 uniform 地 respect 所有 functions f。

11.2 Theorem 3.7

回到 $S, O : 𝒞_{Arith} \to {𝐒𝐞𝐭}_{•}$ 。Theorem 3.7 给出一个 natural transformation：

σ : S \Rightarrow O

$𝒞_{Arith}$ 只有一个 object $*$ ，因此只需要一个 component：

σ_{*} : S (*) \to O (*)

由于 $S (*) = (D, err)$ 、 $O (*) = (𝒫 (ℚ_{\geq 0}), \emptyset)$ ，它的 underlying map 是：

σ_{*} : D \to 𝒫 (ℚ_{\geq 0})

对 $a \in ℚ_{\geq 0}$ ，先定义普通 map：

η (a) = {a}

再用 Lemma 2.9 的 extension construction 把它延拓成 based map：

σ_{*} (a) = {a}

σ_{*} (err) = \emptyset

正常 denotational value 对应 operational result singleton；err 对应没有正常 result，也就是 $\emptyset$ 。

要证明 $σ : S \Rightarrow O$ 是 natural transformation，对每个 context c，必须让下面的 square commute：

O c \circ σ_{*} = σ_{*} \circ S c

对 $a \in ℚ_{\geq 0}$ ，左边是：

(O c) (σ_{*} (a)) = (O c) ({a})

(O c) ({a}) = {b \in ℚ_{\geq 0} ∣ c [a] ⇓ b}

因此需要证明：

{b \in ℚ_{\geq 0} ∣ c [a] ⇓ b} = σ_{*} (ℰ ⟦ c [a] ⟧)

左边是 operational semantics 能执行到的正常结果；右边把 denotational result 转成 O 的 representation。这里 naturality formalise 的，就是两种 semantics 对同一个 context 的 compatibility。

11.3 Lemma 3.8

对于所有 contexts c 和 $a \in ℚ_{\geq 0}$ ，有三条：

1. 如果 $ℰ ⟦ c [a] ⟧ = err$ ，就不存在 b ∈ ℚ≥0 满足 $c [a] ⇓ b$ 。Denotational semantics 是 error 时，operational semantics 不会得到正常 result。

2. 如果 $ℰ ⟦ c [a] ⟧ \in ℚ_{\geq 0}$ ，那么：

c [a] ⇓ ℰ ⟦ c [a] ⟧

也就是 denotational semantics 得到的正常 value，operational semantics 确实能执行到。

3. Big-step operational semantics 是 deterministic：如果 $c [a] ⇓ b$ 和 $c [a] ⇓ b′$ 都成立，那么 $b = b′$ 。同一个 expression 不会有两个不同的 results。

Proof idea：先证明 item 3：从 big-step rules 出发，对 derivation 做 induction，对齐同一个 expression 的两次推导。再把 item 1 / 2 放在一起，对 context c 做 structural induction。每个 constructor 都利用子 context 的结论，以及对应的 denotational definition 和 operational rule。不需要额外的结构。

Case 1： $ℰ ⟦ c [a] ⟧ = err$ 。由 Lemma 3.8 item 1，没有正常 b 满足 $c [a] ⇓ b$ ，所以：

(O c) ({a}) = \emptyset = σ_{*} (err)

Case 2： $ℰ ⟦ c [a] ⟧ \in ℚ_{\geq 0}$ 。Item 2 保证能执行到这个结果，determinism 保证没有其他不同的正常结果，因此：

(O c) ({a}) = {ℰ ⟦ c [a] ⟧}

{ℰ ⟦ c [a] ⟧} = σ_{*} (ℰ ⟦ c [a] ⟧)

输入 err 时，因为 Sc 和 Oc 都是 based maps，两条 path 也都落到 $\emptyset$ 。因此自然性在整个 D 上成立。

Normal case 的集合相等可以拆成两个 inclusions。其中： $σ_{*} (ℰ ⟦ c [a] ⟧) \subseteq (O c) ({a})$ 对应 Lemma 3.8 item 2。这里把这个方向称为 denotational semantics 的 soundness：它给出的正常结果，operational semantics 确实能够执行出来。另一方向还要用 determinism，保证 operational result set 没有额外的不同结果。

11.4 Example 3.9

定义 functor：

F : 𝐒𝐞𝐭 \to {𝐒𝐞𝐭}_{•}

F (X) = (𝒫 (X), \emptyset)

对于 $f : X \to Y$ ，在 morphisms 上取 direct image：对 $U \subseteq X$ ，

(F f) (U) = {f (x) ∣ x \in U}

现在考虑 $α_{X} : F (X) \to E (X)$ ，其中 E 是 Lemma 2.9 中 adjoin a base point 的 functor。这里把 E(X) 的底层集合写成 $X ⊔ {*}$ ：新 base point 记作 ∗，原元素仍用原名，只是对前面的 tagged construction 重新命名。

α_{X} (\emptyset) = *

如果 $U \neq \emptyset$ ，就从 U 中选一个元素。选定之后，每个 component 单独看是 based map，但放到整个 diagram 里就不一定行。

取教材的例子：

X = {0, 1}

Y = {2, 3}

两边都规定选 minimum，所以 $α_{X} (X) = 0$ 、 $α_{Y} (Y) = 2$ 。定义 $f : X \to Y$ 为：

f (0) = 3

f (1) = 2

先选再映射：

(E f) (α_{X} (X)) = (E f) (0)

(E f) (0) = f (0) = 3

先取 direct image 再选：

α_{Y} ((F f) (X)) = α_{Y} (Y) = 2

因为 $3 \neq 2$ ，

E f \circ α_{X} \neq α_{Y} \circ F f

Naturality square 不 commute。问题不是单独的 $α_{X}$ 不合法，而是“从集合中选一个 element”这个 choice 不能 uniform 地 respect arbitrary functions f。因此这组 maps 不是 natural transformation。

Objects morphisms Objects

Categories functors Categories

Functors natural transformations Functors

Material: Henning Basold, Two Voice Semantics · GitLab