语义学讲义: 始代数和终余代数方面

摘要

这些讲义为计算机科学专业的学生提供了一个形式语言的数学语义的非标准介绍. 我们并不试图给出平衡的处理, 而是专注于一些关键的一般性思想, 并用简单的例子加以刻画. 这些思想使用一些基本的范畴论概念来表述. 所有需要的范畴论知识都会在讲义中介绍. 除了为人熟知的句法和语义的始代数方法之外, 我们还会检视不那么为人熟知的操作语义的终余代数方法. 我们对形式语义的处理旨在对于更为标准的介绍进行补充.

引论

这些讲义主要旨在为计算机科学专业的学生介绍形式语言的数学语义的某些方面. 这些讲义并不试图在任何意义上对该领域进行综述, 而是聚焦于一簇与这样的观念相关的想法, 即句法和语义在某种意义上是相互对偶的. 为了表达这一观念, 我们需要使用范畴论中的一些基本概念. 因此, 这些讲义的次要目标是给出对于主要目的而言必要的那些范畴论概念的介绍.

这些讲义只是给出了对于语义学和基本的范畴论的部分介绍. 但是, 我相信将这两个主题结合起来进行介绍能够有效地对于更为标准的介绍进行实用的补充. 至于那些对于这两个主题均有所熟悉的人而言, 我希望这里仍然有些新颖的内容能够吸引你.

暑期学校里我进行了四次讲座. 这篇论文大致遵循着讲座的组织方式, 一章对应于一次讲座. 但是有的部分似乎应该为讲座所给出的内容补充额外的细节. 第一次讲座提供了对于数学语义的介绍. 其引入了一些最为简单的抽象句法例子以及与之相伴的结构的概念, 这些东西是为了对于之后讲座所使用的抽象定义进行形象刻画. 第二次讲座引入了范畴的概念, 用以刻画范畴的例子是结构的范畴, 以及集合的范畴. 第三次讲座引入了这些讲座的中心思想: 集合范畴上的有界标准自函子的概念, 自函子的代数和余代数范畴的概念, 始代数和终余代数的概念. 关于始代数和终余代数的存在性有两个重要的一般性定理. 对于始代数定理, 我们给出了大致的证明思路, 但是对于终余代数定理, 我们没有给出任何证明. 转而在(第三次)讲座的最后一部分, 我们描述了与第一次讲座所给出的四个抽象句法的例子相关的三个终余代数. 第四次也就是最后一次讲座关心的是进程的终宇宙. 讲座讨论了三种类型的计算范式: 传统的非交互确定性计算范式, 两个交互性的确定性计算范式, 以及一个交互性的非确定计算范式. 对于每个情形, 我们都使用了一个有界标准自函子, 而一个终余代数给出了这个范式的进程的终宇宙. 我所使用的交互性非确定范式在强双模拟下与CCS相关联, 但是对于这个事实我只有时间给出草略的图景.

这些讲座里用以刻画想法的都是非常简单且为人熟知的例子. 由抽象句法所给出的句法表达式宇宙和归纳数据类型之间存在着紧密的联系. 这些例子可以看成是归纳数据类型, 但我是以形式语言的术语呈现它们的. 对偶地, 对于终余代数的讨论可以用余归纳数据类型的语言重述.

第1章 数学语义

第1.1节 对于语义学的一般介绍

句法和语义这两个学科之间的区别起源于对于自然语言的研究. 句法关心的是语言的表达式的形式的结构性质, 通常对于其意义毫不在意. 在语义学中, 注意力集中于表达式的意义上. 自然语言在自然中出现, 一般经过了漫长的时间演化. 它们的句法和语义通常只是隐式给出的, 因而有必要通过观察语言的实际使用来建立对于其句法和语义的理解. 这是语言学研究的一部分内容.

与之形成的对比的是, 形式语言, 也就是这些讲义所关心的对象, 是显式的构造, 并且通常拥有显式刻画的句法, 而且理想情况下拥有显式的语义. 形式语言的范例最初出现于逻辑学领域. 它们是经典的命题演算和谓词演算, 以及无数变体和扩展. 形式语言也用于语言学, 其可能扮演着理论性的角色, 作为自然语言的片段的模型出现, 这类似于物理科学中所使用的数学模型.

在计算机科学中形式语言的最直接例子是编程语言. 计算机科学里形式语言的想法有着更为广阔的应用, 不单单是应用于编程语言. 但是对于我们的目的而言, 我们暂时只考虑编程语言就够了.

从历史上来说, 编程语言的设计者没有必要通过给出全然精确的显式句法和语义来描述他们的语言. 他们可以对于一个特定的机器构造一个编译器 (或者一个解释器), 然后编写一个手册给出可以在这个机器上运行的以该语言写成的示例程序. 一个程序员可以通过阅读手册来学习语言, 也可以通过不断试错或者专家的帮助来学习. 以这种方式可用的编程语言在某种意义上就像自然语言. 为了取得对于这种语言更为深刻的理解, 或许有必要更仔细地检视语言并构造显式的句法和语义, 其比运行在特定机器上的编译器更加抽象和理论化.

关于为什么我们想要对于编程语言进行更为深刻和抽象的理解存在着诸多理由. 但是这里我们不会讨论理由. 或许这么说就足够了, 因为对于句法和语义的数学研究的进步, 现在从原则上将编程语言的设计呈现为由精确的句法和语义构成的数学对象成为可能.

形式语言

一个形式语言具有一个句法, 其刻画了语言的表达式的句法范畴, 它还有一个语义, 其刻画了对于句法的一些可能解释, 这赋予了语言的表达式以意义. 有时存在一个突出的解释, 其或许可以称为意图或者说标准解释, 其他的则被称为非意图的或者非标准的. 一个形式语言可能只有单独一个意图解释, 之后才会考虑其他可能的解释. 也可能提供形式语言的时候就没有给出语义, 或者甚至是语义为空, 没有提供解释. 由逻辑学家所研究的未经解释的形式系统, 是这样的例子.

与其专注于单独一个形式语言, 其有着单独一个句法和可能多个解释, 不如把注意力放在一族形式语言的意图解释的统一方法上. 这些讲义的一个主题是在精确的范畴论意义下, 第二种想法可以视为对偶于第一种想法.

运用范畴论, 我们想要检视两个对偶的主题, 其中每个主题都需要选择一个自函子:

1. 对于形式语言的抽象刻画, 通过聚焦于句法的抽象表示作为自函子代数的范畴的始对象, 其解释也被表示为范畴的对象而意义函数则是箭头.
2. 对于表示一族形式语言的每个的意图解释的特定统一方法的刻画, 作为自函子余代数的范畴的终对象, 其每个语言的句法也被表示为范畴的对象而意义函数则是箭头.

当然了, 上述主题对于尚不熟悉范畴论术语的读者而言可能并不清晰. 但是所有的术语都会在这些讲座里介绍.

这些讲义的主题是数学语义. 讨论一个形式语言的一个直接语义是有可能的. 例如, 我们可能想要建立一个用于数学基础的形式语言. 在这种情况下, 我们所想要的是一个直接的先于数学的语义 (pre-mathematical semantics), 其和数学语义相当不同, 因为后者基本上是将形式语言的句法翻译为我们的数学语言. 类似地, 我们可以区分我们对于我们母语的直接理解和通过翻译所得到的对于外语的理解.

第1.2节 句法和语义的例子

这些讲义里我们将会专注于四个非常简单的带有句法和语义的形式语言的例子. 它们是不切实际的简单, 以至于我们可以看到清晰的一般想法而不被更为现实的例子的细节所迷惑. 在每种情形下我们都给出了一个抽象句法, 其确定了一个表达式的集合$E$, 我们还会给出一个与之相关的数学结构概念, 并且对于每个这样的结构$\mathcal{A}=(A,\dots )$, 还要给出一个意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}:E\to A$. 结构的第一个分量是$A$是一个集合, 其被称为结构的潜在集合 (underlying set). 于是, 意义函数将每个表达式与潜在集合中的一个值关联起来. 数学结构是形式语言的解释. {译注: 解释的结果而非解释的过程.} 意义函数是由结构递归定义的, 其遵照表达式生成的方式; 即这个函数被刻画为满足定义性等式 (复数) 的唯一函数, 每种表达式的形式都有一个等式.

在第二个和第三个例子里我们会假设给定了一个固定的集合$K$. 在第四个例子里, 我们假设给定了一个签名, 其由一个函数符号的集合$\mathrm{\Sigma }$构成, 每个$\sigma \in \mathrm{\Sigma }$都有一个与之关联的自然数$n_{\sigma }$作为其元数 (arity).

Peano结构

一个Peano结构$\mathcal{A}=(A,a,f)$由一个集合连带着$a\in A$和$f:A\to A$构成. 这个例子的表达式集合$E$由以下抽象句法给出:$$e⩴◻|e^{+}$$于是$E=\{◻,{◻}^{+},{{◻}^{+}}^{+},\dots \}$. 给定一个Peano结构$\mathcal{A}=(A,a,f)$, 意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}$是唯一的函数$⟦\phantom{\cdot }⟧:E\to A$满足$$\{\begin{array}{ccc}⟦◻⟧& =& a\\ ⟦e^{+}⟧& =& f(⟦e⟧)& (e\in E)\end{array}$$

列表结构

给定一个集合$K$, 一个$K$上的列表结构$\mathcal{A}=(A,a,f)$由一个集合$A$连带着$a\in A$和$f:K\times A\to A$构成. 这次表达式的集合$E$是由以下抽象句法给出的:$$e⩴\mathrm{[]}|k:e,(k\in K)$$$E$的一个典型元素具有形式$k_1:\cdots :k_n:\mathrm{[]}$, 其中$k_1,\dots ,k_n$都是$K$的元素. 给定一个列表结构$\mathcal{A}=(A,a,f)$, 意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}$是唯一的函数$⟦\phantom{\cdot }⟧:E\to A$满足$$\{\begin{array}{ccc}⟦\mathrm{[]}⟧& =& a\\ ⟦k:e⟧& =& f(k,⟦e⟧)& (k\in K,e\in E)\end{array}$$

Lisp结构

给定一个集合$K$, 一个$K$上的Lisp结构$\mathcal{A}=(A,a,f)$由一个集合$A$连带着$a:K\to A$和$f:A\times A\to A$构成. 表达式集合$E$由以下抽象句法给出:$$e⩴k|e\cdot e,(k\in K)$$给定一个Lisp结构$\mathcal{A}=(A,a,f)$, 意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}$是唯一的函数$⟦\phantom{\cdot }⟧:E\to A$满足$$\{\begin{array}{cccc}⟦k⟧& =& a(k)& (k\in K)\\ ⟦e_1\cdot e_2⟧& =& f(⟦e_1⟧,⟦e_2⟧)& (e_1,e_2\in E)\end{array}$$

$\mathrm{\Sigma }$-结构

给定一个签名$\mathrm{\Sigma }$, 一个$\mathrm{\Sigma }$-结构$\mathcal{A}={(A,{\sigma }^{\mathcal{A}})}_{\sigma \in \mathrm{\Sigma }}$由一个集合$A$连带着对于每个$\sigma \in \mathrm{\Sigma }$的${\sigma }^{\mathcal{A}}:A^{n_{\sigma }}\to A$构成. 当$n_{\sigma }=0$时, $A^{n_{\sigma }}$是一个单元素集合, 其由一个空元组构成, 于是${\sigma }^{\mathcal{A}}$不过就是挑选$A$的某个元素${\sigma }^{\mathcal{A}}()$. 根据惯例此时我们将${\sigma }^{\mathcal{A}}$与这个元素视为等同的. 表达式集合$E$由以下抽象句法给出:$$e⩴\sigma \stackrel{\stackrel{n_{\sigma }}{⏞}}{e\cdots e},(\sigma \in \mathrm{\Sigma })$$给定一个$\mathrm{\Sigma }$-结构$\mathcal{A}={(A,{\sigma }^{\mathcal{A}})}_{\sigma \in \mathrm{\Sigma }}$, 意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}$是唯一的函数$⟦\phantom{\cdot }⟧:E\to A$满足$$⟦\sigma e_1\cdots e_{n_{\sigma }}⟧={\sigma }^{\mathcal{A}}(⟦e_1⟧,\dots ,⟦e_{n_{\sigma }}⟧),(\sigma \in \mathrm{\Sigma },e_1,\dots ,e_{n_{\sigma }}\in E)\text{.}$$

第1.3节 关于结构归纳和结构递归的讨论

考虑到有的读者可能不熟悉可用于抽象句法的结构归纳和结构递归, 我们以其与第四个例子$\mathrm{\Sigma }$-结构的关联来回顾这些想法. 已经熟悉了的读者可以将这个间章视为填充细节的拓展练习.

一个句法等式$e⩴\cdots$, 对于表达式$e$的集合$E$而言, 刻画了$E$的一个归纳定义. 在我们的第四个例子里, $E$被归纳地定义为满足对于每个$\sigma \in \mathrm{\Sigma }$, 有$$e_1,\dots ,e_{n_{\sigma }}\in E\Rightarrow \sigma e_1\cdots e_{n_{\sigma }}\in E$$的最小集合. 这个归纳定义可以重述为以下的显式定义:$$E=E^0\cup E^1\cup \cdots$$其中$E^k$是由等式$E^0=\varnothing$和对于$k\in \mathbb{N}$,$$E^{k+1}=\{\sigma e_1\cdots e_{n_{\sigma }}|\sigma \in \mathrm{\Sigma },e_1,\dots ,e_{n_{\sigma }}\in E^k\}$$原始递归地定义的. 注意到根据数学归纳法, 可得$E^0\subseteq E^1\subseteq E^2\subseteq \cdots$.

第1.4节 结构的例子

Peano结构

标准的例子是$(\mathbb{N},0,s)$, 其中$\mathbb{N}=\{0,1,2,\dots \}$是自然数集, 而对于$n\in \mathbb{N}$有$s(n)=n+1$. 另一个我们之后会感兴趣的例子是$({\mathbb{N}}^{\infty },0,s^{\infty })$, 其中${\mathbb{N}}^{\infty }=\mathbb{N}\cup \{\infty \}$而$$s^{\infty }(n)=\{\begin{array}{cc}s(n)& \text{, 如果}n\in \mathbb{N}\hfill \\ \infty & \text{, 如果}n=\infty \hfill \end{array}\text{.}$$这里的$\infty$是一个不在$\mathbb{N}$之中的对象.

列表结构

我们将取$(K^{⁎},ϵ,\mathrm{cons})$作为我们的标准例子, 其中$K^{⁎}$是由$K$的元素的所有(有限的)字符串$\rho =k_1\cdots k_n$构成的集合, $ϵ$是空字符串, 而$$\mathrm{cons}(k,\rho )=k{k}_1\cdots k_n$$其中$k\in K$而$\rho =k_1\cdots k_n\in K^{⁎}$.

我们也会对于可能无穷的字符串的列表结构$(K^{\infty },ϵ,{\mathrm{cons}}^{\infty })$感兴趣. 这里$K^{\infty }=K^{⁎}\cup K^{\omega }$, 其中$K^{\omega }$是由$K$的元素的无穷字符串$\rho =k_1{k}_2\cdots$构成的集合, 而$${\mathrm{cons}}^{\infty }(k,\rho )=k{k}_1\cdots$$其中$k\in K$而$\rho =k_1\cdots \in K^{\infty }$.

Lisp结构

给定集合$K$, 标准的例子是Lisp结构$(𝕊,\mathrm{atom},\mathrm{dot})$, 其中$𝕊$是Lisp的$S$-表达式的集合, 而$S$-表达式由对于每个$k\in K$的原子$\mathrm{atom}(k)$通过点对 (dotted pairing) 操作$\mathrm{dot}$构建而成, $\mathrm{dot}$将两个$S$-表达式$M_1,M_2$和一个$S$-表达式$M_1\cdot M_2$联系起来.

我们也对于带有可能循环或者无限的$S$-表达式的Lisp结构感兴趣. 这些表达式可以被视为叶子以$K$的元素所标记的特定种类的二叉树. 给出一个对于这些树的精确集合论定义是有用的. 我们从更一般的$S$-预树的概念开始. 这些对象被定义为序对$M=(|M|,l_M)$, 其中$|M|\subseteq {\{1,2\}}^{⁎}$而$l_M:|M|\to K\cup \{\cdot \}$. 这里的$\cdot$是某个不在$K$之中的对象. 令$\mathbb{PS}$是由这些预树构成的集合. 如果$k\in K$, 令$\mathrm{atom}(k)$是由$$\{\begin{array}{ccc}|M|& =& \{ϵ\}\\ l_M(ϵ)& =& k\end{array}$$所给出的预树$M$. 如果$M_1,M_2$是预树, 令$M_1\cdot M_2$是由

$\mathrm{\Sigma }$-结构

第1.5节 句法作为结构

在我们四个句法和语义的例子里, 我们都可以根据表达式集合$E$构造一个结构$Ɛ=(E,\dots )$. 我将其称为句法结构 (syntax structure).

第2章 结构的范畴

第2.1节 范畴

这一节我们将引入范畴的概念. 我们初始的启发性例子是集合与集合之间的函数的范畴.

集合之间的函数

如果$A,B$是集合, 那么我们记$f:A\to B$, 如果$f$是一个从$A$到$B$的函数. 集合$A$被称为$f$的定义域 (domain)而集合$B$被称为$f$的陪域 (codomain). 对于每个$x\in A$, 应用 (apply)$f$于$x$的结果$f(x)$在$B$之中. 当陪域和值域 (range)$\{f(x)|x\in A\}$重合时, $f$是满射的 (surjective). 但是, 函数不必然是满射的. 因此, 集合论的习惯一样, 函数不能与其图 (graph) 等同起来, 而是需要携带陪域的信息. 这意味着若有$f:A\to B$和$f^{\prime }:A^{\prime }\to B^{\prime }$, 那么$f=f^{\prime }$当且仅当$A=A^{\prime }$, $B=B^{\prime }$, 且对于每个$x\in A$有$f(x)=f^{\prime }(x)$.

如果$A$是一个集合, 那么$A$上的恒等函数${\mathit{id}}_A$是满足${\mathit{id}}_A:A\to A$和对于所有$x\in A$都有${\mathit{id}}_A(x)=x$的唯一函数.

如果$f:A\to B$而$g:B\to C$, 那么$(g,f)$是可复合的 (composable), 而其复合 (composite)$g\circ f$是满足$g\circ f:A\to C$和对于所有$x\in A$都有$(g\circ f)(x)=g(f(x))$的唯一函数.

注记: 如果$f:A\to B$, 那么$$f\circ {\mathit{id}}_A={\mathit{id}}_B\circ f=f\text{.}$$另外, 如果也有$g:B\to C$和$h:C\to D$, 那么$$(h\circ g)\circ f=h\circ (g\circ f)\text{.}$$

定义

集合的范畴

第2.2节 结构的范畴

本节我们将会基于之前所给出的结构概念的四个例子来给出更多的范畴的例子. 在每种情形下, 范畴的对象都是结构, 而箭头是由一对结构和其间一个同态构成的三元组; 也就是说, 是一个结构的潜在集合之间的保持结构的函数. 三元组是必要的, 而不能只是单独的同态, 由此范畴的定义域和陪域运算才能得到定义. 不过在实践中往往忽略箭头和其同态分量之间的区别更为方便.

Peano结构的范畴

范畴$\mathbf{Pea}$以Peano结构作为其对象. 给定Peano结构$\mathcal{A}=(A,a,f)$和${\mathcal{A}}^{\prime }=(A^{\prime },a^{\prime },f^{\prime })$, 从$\mathcal{A}$到${\mathcal{A}}^{\prime }$的一个同态是一个保持结构的函数$\pi :A\to A^{\prime }$, 即$$\{\begin{array}{ccc}\pi (a)& =& a^{\prime }\\ \pi (f(x))& =& f^{\prime }(\pi (x))& (x\in A)\end{array}$$$\mathbf{Pea}$的箭头是由Peano结构和其间的一个同态构成的三元组$(\mathcal{A},\pi ,{\mathcal{A}}^{\prime })$. 这个范畴的运算是什么应该是显然的, 并且成为范畴的条件成立也是显然的. 在其他三个例子里我们只会描述同态的概念.

列表结构的范畴

给定一个集合$K$, 范畴$\mathbf{List}(K)$以$K$上的列表结构为其对象, 而确定了箭头的同态的概念则定义如下. 给定$K$上的列表结构$\mathcal{A}=(A,a,f)$和${\mathcal{A}}^{\prime }=(A^{\prime },a^{\prime },f^{\prime })$, 从$\mathcal{A}$到${\mathcal{A}}^{\prime }$的一个同态是一个函数$\pi :A\to A^{\prime }$满足$$\{\begin{array}{ccc}\pi (a)& =& a^{\prime }\\ \pi (f(k,x))& =& f^{\prime }(k,\pi (x))& (k\in K,x\in A)\end{array}$$

Lisp结构的范畴

给定一个集合$K$, 范畴$\mathbf{Lisp}(K)$以$K$上的Lisp结构为其对象, 而确定了箭头的同态的概念则定义如下. 给定$K$上的Lisp结构$\mathcal{A}=(A,a,f)$和${\mathcal{A}}^{\prime }=(A^{\prime },a^{\prime },f^{\prime })$, 从$\mathcal{A}$到${\mathcal{A}}^{\prime }$的一个同态是一个函数$\pi :A\to A^{\prime }$满足$$\{\begin{array}{cccc}\pi (a(k))& =& a^{\prime }(k)& (k\in K)\\ \pi (f(x_1,x_2))& =& f^{\prime }(\pi (x_1),\pi (x_2))& (x_1,x_2\in A)\end{array}$$

$\mathrm{\Sigma }$-结构的范畴

给定一个签名$\mathrm{\Sigma }$, 范畴$\mathbf{Str}(\mathrm{\Sigma })$以$\mathrm{\Sigma }$-结构为其对象, 而确定了箭头的同态的概念则定义如下. 给定$\mathrm{\Sigma }$-结构

第2.3节 句法结构是始对象

现在我们已经得到了四个结构范畴的例子. 对于这些例子, 我们都已经定义了一个句法结构$Ɛ$. 对于范畴中的每个结构$\mathcal{A}=(A,\dots )$, 都存在着一个意义函数${⟦\phantom{\cdot }⟧}^{\mathcal{A}}:E\to A$, 其由$E$中的表达式形式上的结构递归定义; 也就是说, 其被定义为满足特定等式的唯一函数. 通过观察这些等式, 我们发现它们恰恰就是用于描述从$Ɛ$到$\mathcal{A}$的同态概念所使用的等式. 于是, 我们发现$Ɛ$具有一个特别的性质, 即对于每个结构$\mathcal{A}$, 在结构范畴里存在唯一的箭头$Ɛ\to \mathcal{A}$; 也就是说, 根据以下的定义, $Ɛ$是结构范畴里的一个始对象.

在集合范畴里, 空集$\varnothing$是唯一的始对象. 这是因为对于任意的集合$Y$, 存在唯一的函数$\varnothing \to Y$, 即空函数, 其由序对构成的图就是空集. 注意到范畴不必拥有始对象. 例如, 非空集合的范畴就是这样的. 范畴也不必只有一个始对象. 例如, 在Peano结构的范畴里, 自然数的Peano结构和句法结构不同, 但也很容易看出来是始对象. 尽管这两个结构是不同的, 但是从抽象层面来说它们是相同的, 在于一个结构是另一个结构的复制, 意即存在一个给出了来回两个结构的同态的一一对应, 也就是说两个结构是同构的. 这是关于始对象的一般事实——当存在始对象时, 任意一对始对象之间都存在唯一的同构, 因而是同构的. 我们现在转向范畴中的同构的一般概念.

第2.4节 同构

在抽象数学里, 同构的数学结构被视为在抽象层面上相同. 同构的意思是结构之间存在一对同态, 互为对方的逆. 这种同构的概念可以在任何范畴之中定义.

第2.5节 始对象

抽象数学刻画数学结构只关心同构意义上的, 即所描述的结构上的条件满足

1. 存在满足条件的结构.
2. 任何同构于满足条件的结构的结构都满足条件.
3. 对于任何一对满足条件的结构, 它们都是同构的.

范畴论的一个基本主题是使用所谓的泛映射性质来描述范畴中唯一同构意义上 (up to unique isomorphism)的对象. 这种想法最简单的例子由我们已经定义了的始对象给出.

总结一下, 以下定理刻画了这次讲座的要义. 形式语言的句法和语义的始代数方式在于选择一个范畴使得形式语言的句法可以视为这个范畴的始对象. 然后, 任何语义都应该刻画为范畴里的对象. 这么做了以后, 意义函数就由从(作为始对象的)句法宇宙到表示语义的对象的唯一映射所唯一确定了. {译注: 这里的唯一映射指的是范畴里存在唯一的箭头, 当然指的不是随意的映射.}

第3章 始代数和终余代数

让我们设我们有了一个形式语言, 我们想要选择一个范畴$ℂ$以使得句法可以表示为始对象$I$, 而每个解释可以表示为一个对象$A$, 并且意义函数可以表示为唯一的箭头$I\to A$. 在许多情况下, 例如对于我们的四个例子而言, 范畴$ℂ$可以自然地选取为某个自函子的代数的范畴, 这使用了我们将要引入的术语. 从范畴$ℂ$到范畴${ℂ}^{\prime }$的函子的概念是自然的同态概念, 即范畴之间保持结构的映射.

第3.1节 函子

第3.2节 结构作为代数

自函子的代数

给定某个范畴上的一个自函子$F$, 那么一个$F$的代数是一个序对$(A,\alpha )$, 其中$A$是范畴的一个对象, 而$\alpha :F(A)\to A$. 我们可以构造范畴$\mathbf{alg}(F)$, 其对象是$F$的代数而箭头是这样的代数之间的同态给出的. 如果$(A,\alpha )$和$(A^{\prime },{\alpha }^{\prime })$是$F$的代数, 那么从$(A,\alpha )$到$(A^{\prime },{\alpha }^{\prime })$的一个同态$(A,\alpha )\to (A^{\prime },{\alpha }^{\prime })$是一个函数$\pi :A\to A^{\prime }$满足$$\pi \circ \alpha ={\alpha }^{\prime }\circ F(\pi )\text{.}$${译注: 原文这里是函数, 但是我感觉用箭头一词更为合理.} 于是, 这个范畴的箭头可以取为三元组$((A,\alpha ),\pi ,(A^{\prime },{\alpha }^{\prime }))$, 或者我们也可以使用三元组$(\alpha ,\pi ,{\alpha }^{\prime })$.

我们可以表明, 对于我们的四个结构概念的例子, 我们都可以在集合范畴$\mathbf{Set}$上定义一个自函子$F$以使得每个结构$\mathcal{A}=(A,\dots )$都可以视为一个$F$的代数$(A,\alpha )$. 在以下每种情形里, 我们首先对于每个集合$X$定义$F(X)$, 并且对于集合$X,Y$和每个函数$\pi :X\to Y$定义$F(\pi ):F(X)\to F(Y)$. 我们将验证$F$的确是一个函子的工作留作练习. 最终, 在每种情形里我们都会对于结构$\mathcal{A}=(A,\dots )$定义$\alpha :F(A)\to A$. 不过, 首先我们需要二元无交并和索引无交并的记号.

一些记号: 对于集合$X,Y$我们令$X+Y$为其二元无交并, 使用$0,1$作为标签, 即$$X+Y=(\{0\}\times X)\cup (\{1\}\times Y)\text{.}$$更一般地, 如果${(X_i)}_{i\in I}$是由集合$I$索引的一个集合族, 那么$\sum _{i\in I}{X}_i$是这个族的索引无交并, 即$$\sum _{i\in I}{X}_i=\{(i,x)|i\in I\text{且}x\in X_i\}\text{.}$$在以下的前两个例子中对于函子$F$的定义里, 我们使用$1$代表单元素集$\{0\}$.

第3.3节 始代数

有界标准自函子

始代数定理

第3.4节 终余代数

第3.5节 终余代数的例子

第4章 进程的终宇宙

第4.1节 非交互确定性范式