原文标题：Algebra
作者：Oleg Kiselyov
原文链接：Algebra
代数式副作用（algebraic effects）和代数数据类型（algebraic data type）中的「代数」究竟是什么？哪些模块/对象的签名是「代数」的？「代数」到底是什么？自由代数（free algebra）的「自由」在哪里？初始代数（initial algebra）是什么，它有什么用，我们如何证明一个代数具有「初始性」？我们能准确地描述 tagless-final 式 DSL 嵌入，及其解释器的正确性吗？如果能描述，如何证明这种正确性？
本文以讲义的形式展示了一些泛代数（Universal Algebra）领域的标准入门材料，旨在解答这一类问题。不过，这些材料是专门为程序员，尤其是那些对 tagless-final 方法感兴趣的程序员所挑选和安排的。我们只使用编程中遇到的例子，并尽可能使用具体的编程语言中的符号，而非数学符号。
导言
什么是代数（Algebra）？Garet Birkhoff 被现在的人们誉为「泛代数」领域的创始人，他是这么说的：
By an `abstract algebra’ is meant, loosely speaking, any system of elements and operations such as a ring, a field, a group, or a Boolean algebra.
译：「抽象代数」泛指那些由元素和运算组成的系统：如环、域、群和布尔代数。（Birkhoff，1935）
随后，他又提出了一个「临时用的形式定义」，这一定义现在仍被人们使用（稍后会回顾这些形式定义）。
泛代数是数学的一个领域——关于泛代数的课程和教科书的很大一部分内容是格论（Lattice theory）和组合数学（Combinatorics）。看起来，这似乎与常见的编程任务没有太大联系。但世事无常，造化弄人，自动机（Automata）理论（有限状态机、Kleene 代数、正则表达式）是代数在计算机科学的最早应用之一。根据 Gougen 等人（1977）的说法：Burstall 和 Landin 共著的《Programs and their proofs: An algbraic approach》（1969）首次在编程语言语义学研究中使用了泛代数和（隐含的）代数初始性。F. L. Morris（《Correctness of translations of programming languages》斯坦福大学博士论文，1972 年）则引入了编程语言中最为常见的多类别代数。而在计算机科学中全面引入代数和范畴论技术，应归功于 ADJ 四人帮（J. A. Gougen、J. W. Thatcher、E. G. Wagner 和 J. B. Wright），他们随后还引领了代数数据类型、模块系统和代数规范的发展。特别是在 Gougen 等人（1977）的论文中，他们证明了如何通过初始代数语义统一大量的语义形式，并优雅地回答了「什么是语法（syntax）？什么是语义（semantics）？」的问题。而最近，代数式副作用则再次将「代数」这一概念炒上了风口。tagless-final 方法也是代数在编程中的一种应用，它与初始代数语义密切相关。
本文收集了计算机学家，尤其是 tagless-final 程序员最感兴趣的泛代数定义和标准结果，旨在为这些人提供参考。我们的首要目标是「与编程相关」，这一目标也决定了我们选择的引用材料和标记符号——我们只使用编程例子和具体编程语言的符号（即 OCaml）。在普遍的泛代数数学研究中，人们往往使用依赖于大量上标和下标的符号，而为了避免写出更深的嵌套上下标，还大量使用一些有时令人困惑的重载。编程语言的符号更规范，不那么含糊不清，而且可以通过编译器进行「机械检查」。
事实上，我们不应该对「OCaml 模块的记号适用于描述代数」这一点感到惊讶：Joseph Gougen 对 ML 模块系统的设计产生了重大影响。1
引用文献
- Martin Wirsing: Algebraic specifications
内容全面，但具有强烈的数学风格和范畴风格。本文借用了其中的大部分定义，而更改了记法符号。出自 Handbook of Theoretical Computer Science B, 1990, J. van Leeuwen, Ed. Elsevier. pp 675-788
为数学系研究生所编写的一份标准且详尽的研究生教材。初始代数这一概念在该书中仅作为使用空集生成器的自由代数的一个特例而简要提及。出自 Graduate Texts in Mathematics, 1981, v. 78 10.1007/978-1-4613-8130-3
- J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright: Initial Algebra Semantics and Continuous Algebras
这篇论文在计算机科学领域中正式引入了初始代数，具体见其 1-4 节。出自 Journal of the ACM, Vol 24, No 1, January 1977, pp 68-95
- Bart Jacobs and Jan Rutten: A Tutorial on (Co)Algebras and (Co)Induction
本教程面向计算机科学家，事无巨细地阐释了代数和初始性。该教程还演示了「初始性证明」，并将其作为归纳证明的一种替代方案——通常是一种更简单明了的替代方案。教程中使用了 $Σ$-代数的另一种表述：即所谓的 $F$-代数——这一表述利用多项式函子（polynominal functor）来表示代数签名。出自 EATCS Bulletin, 1997, 62, pp. 222–259
泛代数领域的奠基论文。出自 Proceedings of the Cambridge Philosophical Society, 1935, v31, 433-454
文章附带的完整 OCaml 代码：可执行规范
签名与 Σ 代数
Birkhoff 将（抽象）代数形式化定义为由类 $A$（现称载体（carrier）集合），以及在其之上的一类运算组成：每个运算都与「$A$ 中元素形成的序列」所构成的集合相关联，并将这些序列映射到 $A$ 中的某个元素。我们稍后将看到它在具体编程术语中的含义。
我们将研究的是所谓多类别代数（many-sorted algebra），这种代数的载体集合不止一个，而是多个。为了区分不同载体并方便参照，每个载体集合都与自己的类别（sort）相关联，我们可以将「类别」看作一个给载体命名的符号。对于多类别代数，习惯上首先会定义一个代数的签名（signature），这里先给出形式化定义，稍后再作解释
定义. 多类别代数签名 $Σ$ 是一个有序对 $⟨S,F⟩$。其中 $S$ 代表由类别组成的集合，$F$ 代表由函数组成的集合，且存在 $n≥0$，使两者满足映射 $F↦S^{n}×S$。
对于 $F$ 中特定的函数 $f$ ，这样的映射通常表示为 $f\colon s_{1}…s_{n}→s$，其中 $\left\{s,s_{1},…,s_{n}\right\}⊂S$（Wirsing，1990）。数字 $n$ 表示函数 $f$ 的「参数数量」，零参的运算则称为常量。
Wirsing 的定义是对 Birkhoff 最初定义的直接推广，使之适用于多类别的情况（同样，也是对 Birkhoff 定义的一种限制：Birkhoff 允许定义具有无穷个参数的运算，也允许定义载体和运算不是集合，而是真类的代数）。
在编程语言术语中，多类别代数签名就是模块签名。试举一例
module type NAT = sig
type nat
val zero : nat
val succ : nat -> nat
val plus : nat * nat -> nat
end
这里类别的集合 $S$ 是 nat 的单例集 {nat}，集合 $F$ 则由三个元素组成：{zero, succ, plus}，它们之间有如下映射
zero ↦ nat
succ ↦ nat × nat
plus ↦ (nat × nat) × nat
而这些映射可以用 OCaml 声明（更精确地）表示为：
val zero : nat
val succ : nat -> nat
val plus : nat * nat -> nat
所谓的「类别」，在编程语言中就是「类型」（Jospeh Gougen 曾认为「类型（type）」一词太含糊，所以他们选择了「类别（sort）」一词。无论对（OCaml）程序员而言听起来多么奇怪，我们也坚持使用「类别」这个词。）
练习 1. 试举一些符合 OCaml 模块签名定义，但是不符合代数签名定义的例子。
有了签名 $Σ$ 的定义，我们就可以定义什么是 $Σ$-代数
定义. $Σ$-代数是一个有序对 $⟨ \left\{A_{s(s∈S)}\right\},\mathcal{F} ⟩$。其中 $\left\{A_{s\left(s∈S\right)}\right\}$ 是类别集合 $S$ 中所有类别的载体集合构成的集合族，而集合 $\mathcal{F}$ 对于 $F$ 中所有函数 $f\colon s_{1},…,s_{n}→s$ 都有对应的完全（total）函数 $f^{A}\colon A_{\left\{s_{1}\right\}},…,A_{\left\{s_{n}\right\}}→A_{s}$。（Wirsing，1990）
下面是一个 NAT-代数的例子：
module NatUL = struct
type nat = unit list
let zero = []
let succ x = () :: x
let plus (x,y) = x @ y
end
鉴于 NAT 只有一个类别，代数 NatUL 也就只有一个载体集合，即 unit list 集合 {[], [()], [();()], ...}。其中常量 zero 是空列表；succ 则通过「添加一个 ()」 ，将列表映射为一个更长的列表；plus 将一对列表映射为它们的连接。succ 和 plus 可以处理任何列表参数，无一例外。
下面是另一个 NAT-代数：
module NatBool : (NAT with type nat = bool) = struct
type nat = bool
let zero = false
let succ x = not x
let plus (x,y) = not (x = y) (* 异或 *)
end
这一代数的载体集合是布尔集合。我们为模块添加了类型声明，这样 OCaml 就可以检查它是否实现了 Nat 签名所需的所有操作。我们还公开了这一特定代数载体集合的类型（即抽象类别 nat 与具体载体类型之间的关联）。
从现在起，我们将使用 OCaml 符号：OCaml 签名代表代数签名 $Σ$，实现了特定签名的 OCaml 模块代表相应的代数。
代数同态
所谓代数同态（Algebra Homomorphism），就是具有相同签名的两个代数之间的映射。具体而言，是一个代数的载体集合到另一个代数的相应载体集合之间，且「保留了其上的运算」的映射。下面给出它的形式化定义
定义. 令 S 为一代数签名（其签名具有类别 s1, s2, ..., sk 和运算 f1, f2, ..., fm），令 M1: S 和 M2: S 为两个 S-代数，即满足签名 S 的两个模块。M1 与 M2 之间的同态 H12（记作 H12: M1 ~> M2）是由函数 h_s1, ..., h_sk 构成的集合，每个函数都对应于一个类别。
这一定义可以用下面的 OCaml 签名表示：
module H12 : sig
val h_s1: M1.s1 -> M2.s1
val h_s2: M1.s2 -> M2.s2
...
val h_sk: M1.sk -> M2.sk
end
函数 h_si (i=1..k) 不一定是单射（injective）或者满射（surjective），但它们必须是完全函数：h_si : M1.si -> M2.si 应当可以处理所有被集合 M1.s1 接受为参数的值。此外，函数 h_si 还必须「保留其运算」：对于有 n 个参数的运算 f : s_1 ... s_n -> s，对于所有 a_1 ∈ M1.s1, ...，a_n ∈ M1.sn 都要满足等式
h_s (M1.f (a_1, ..., a_n)) = M2.f (h_s1 a_1, ..., h_sn a_n)
任何代数都存在一个到其自身的同态：恒同态（identity morphism），可写作 Id。这一同态是载体集合的恒同映射（identity mapping），显然也保留了其上的运算。
更有趣的是一个 NatUL 到 NatBool 的同态：
module HULtoBool : sig val h : NatUL.nat -> NatBool.nat end = struct
let rec h = function
| [] -> false
| _ :: t -> not (h t)
end
这里「保留其运算」的具体条件是
h NatUL.zero = NatBool.zero
h (NatNUL.succ x) = NatBool.succ (h x)
h (NatUL.plus (x,y)) = NatBool.plus (h x, h y)
对于任意的 unit list 类型的值 x 和 y，同态显然都满足这些条件。通过代入 h 和代数的运算定义就不难证明这点，读者不妨自行观察。
练习 2. 证明不存在从 NatBool 到 NatUL 的同态。
练习 3. 考虑另一个 NAT-代数
module NatStr : (NAT with type nat = string) = struct
type nat = string
let zero = "Z"
let succ x = "S" ^ x
let plus (x,y) = "(" ^ x ^ + ^ y ^ ")"
end
是否存在从 NatStr 到之前引入的代数的同态关系？请注意，NatStr 的载体集合是全体 OCaml 字符串组合的集合（其中不仅包括 "SZ"，还包括 "foo"）。是否有办法调整 NatStr，使其存在到 NatUL 的同态关系？
同态本质上是一系列将「某代数的载体映射到别的代数的载体」的函数。函数应当可以组合，我们将函数组合的符号 $・$ 也应用于同态组合上。
定理. 若 H1: M1 ~> M2 以及 H2: M2 ~> M3 是两个同态，它们的组合 H2 ・ H1 是一个从 M1 到 M3 的同态。
证明. 易证 H2 ・ H1 可以将 M1 的载体集合映射到 M3 的载体集合。而要证明函数保留了其运算，那么对于任意的 f : s_1,...,s_n -> s 有
(H2.hs ・ H1.hs) M1.f(x_1,...,x_n)
= H2.hs (H1.hs (M1.f(x_1,...,x_n)))
= H2.hs (M2.f(H1.hs1 x_1,...,H1.hsn x_n))
= M3.f(H2.hs1 (H1.hs1 x_1),...,H2.hsn (H1.hsn x_n))
= M3.f((H2.hs1 ・ H1.hs1) x_1,...,(H2.hsn ・ H1.hsn) x_n)
$\blacksquare{}$
若同态 H: M1 ~> M2 是满射——即 M2 载体集合中的每个元素都是 M1 载体的某个元素通过 H 得到的「像」，那么我们称代数 M2 是 M1 的同态映像（homomorphic image）。例如同态 HULtoBool 是一个满射，那么 NatBool 是 NatUL 的同态映像。
如果同态 H: M1 ~> M2 中所有载体映射函数都是一一对应的（即同时是单射和满射），这种同态可以称为同构（isomorphism），且 M1 与 M2 互相同构。Id 同态实际上就是一个同构。
定理. 对于同态 H: M1 ~> M2，当且仅当存在同态 H': M2 ~> M1 满足 H ・ H' = Id 和 H' ・ H = Id 时，H 和 H' 是同构。
证明. 留作读者练习。 $\blacksquare{}$
初始代数
正如我们所见，代数同态关系并不总是存在。而我们现在要构建一个代数，从这个代数到其他相同签名的代数总是存在同态关系，而且只有唯一的同态关系。我们用先前定义的 NAT 签名来展示这一构造。令 TFc 为 OCaml functor 组成的集合。
module type TF = functor(N: NAT) -> sig val e : N.nat end
先构造一个属于 TFc 集合的 functor
module TFzero(N: NAT) = struct let e = N.zero end
设 functor T1 为 TFc 集合中的元素，那么有
module TS(N: NAT) = struct
let e = let module M1 = T1(N) in
N.succ M1.e
end
可以简化如下
module TS(N: NAT) = struct let e = N.succ T1(N).e end
（在当前版本的 OCaml 中，必须将 T(N).e 写作 let module M = T(N) in M.e，详情请参阅附带代码。）再设 functor T1 和 T2 为 TFc 中元素，那么有
module TP(N: NAT) = struct let e = N.plus (T1(N).e, T2(N).e) end
构造完毕。
下面则展示了另外一种写出集合 TFc 中元素的方法：
module TFN(N: NAT) = struct
open N
(* 仅使用运算 succ，zero 和 plus 构造而成的项 *)
let e = plus (succ zero, succ (succ zero))
end
对使用过 tagless-final 的读者而言，这应该很熟悉。
通过添加一些显而易见的的运算，可以将 TFc 转化为一个 NAT-代数：
module TFC : (NAT with type nat = (module TF)) = struct
type nat = (module TF)
let zero = (module TFzero : TF)
let succ (module T1: TF) : nat =
(module (functor (N: NAT) -> struct
let e = N.succ T1(N).e
end))
let plus ((module T1: TF), (module T2: TF)) : nat =
(module (functor (N: NAT) -> struct
let e = N.plus (T1(N).e, T2(N).e)
end
end
之前展示的样例元素 TFN 现在可以写为
module TFCsample: TF =
(val let open TFC in plus (succ zero, succ (succ zero)))
对于任意 NAT-代数 N，必定存在一个从 TFC 到该代数的同态：
module HTFC(N: NAT) = struct
let h : TFC.nat -> N.nat = fun (module T: TF) -> T(N).e
end
在下面的证明中，我们设 N 为任意 NAT-代数，h 为 HTFC(N).h，那么有 fun (module T: TF) -> T(N).e。显然，h 将载体集合 TFc 中的所有元素（即所有 functor TF）映射到 N.nat 的某些元素上。例如：TFN 会被映射到 TFN(N).e，即用 N 上的 zero、succ 和 plus 运算计算得到的 N.nat 类型的结果，如下示：
let open N in let e = plus (succ zero, succ (succ zero))
现在我们已经知道 h 是一个完全映射，现在我们证明它是否保留了其上的运算，即对于 TFc 中的任意 x 和 y，都满足：
h TFC.zero = N.zero
h (TFC.succ x) = N.succ (h x)
h (TFC.plus (x, y)) = N.plus (h x, h y)
证明. 展开定义
h TFC.zero = h (module TFzero) = TFzero(N).e = N.zero
h (TFC.succ x) =
let (module T1: TF) = x in
h (module (functor (N: NAT) -> struct let e = N.succ T1(N).e end
= let (module T1: TF) = x in N.succ T1(N).e
= N.succ (h x)
plus 运算读者自证不难。 $\blacksquare{}$
由于 TFC 从构造上就保证了「保留其运算」这一性质，所以证明本身是非常平凡的。
现在我们证明：h 是从 TFC 到 N 的唯一同态映射
证明. 设从 TFc 到 N.nat 还有另一个能保留运算的映射，称为 g。由于 h 和 g 都必须保留 zero 运算。
h TFC.zero = N.zero = g TFC.zero
即，h 和 g 在 TFC.zero 上等价。如果 h 和 g 将 TFc 中的 t 映射到 NAT.nat 中的同一元素，那么它们也必须在 TFC.succ t 上等价，类似方法可推广到 TFC.plus 上。根据结构归纳法，h 和 g 在 TFc 的所有元素上等价。因此，h 是唯一的。 $\blacksquare{}$
定义. 若某 $Σ$-代数与其他具有相同签名的代数都具有唯一的同态，那么称这一 $Σ$-代数为初始代数（initial algebra）。
上面展示的 TFc 是一个标准构造，Birkhoff 也利用这一构造来证明存在初始代数（事实上，他探讨的是自由代数（free algebra），这种代数是初始代数的一个特例）。像 TFc 这样构造的载体集合称为 $Σ$-签名的 Herbrand 宇宙（Herbrand Universe）（参见逻辑编程中的 Herbrand 宇宙和Herbrand 基（Herbrand basis）），而 TFC 代数本身则被称为字代数（word algebra）或基项代数（ground-term algebra）。不难将这种构造方式推广到多类别的情况，从而得到：
定理. 对于任意代数签名 $Σ$，若其 Herbrand 宇宙包含了其所有类别的项，那么该签名必定存在一个初始 $Σ$-代数。
练习 4. NatBool 不是一个初始 NAT-代数（为什么？）。请证明 NatUL 也不是一个初始 NAT-代数。（提示：证明不存在 NatUL 到 TFC 的同态）
练习 5. （这一练习并不完全直观）虽然 NatUL 无法成为初始 NAT-代数，但仍有一个具有和 NatUL 相同载体集合（即 unit list）的初始 NAT-代数，尝试构建之。
练习 6. 使用 OCaml 函数，而非 functor 来构建初始 NAT-代数（函数可以将模块作为其参数）。
定理. 具有相同签名的两个初始代数互相同构。
证明. 令 M1、M2 为两初始代数。那么存在（唯一）同态 H12: M1 ~> M2 和 M21: M2 ~> M1，它们的组合 H21 ・ H12: M1 ~> M1 也是同态。我们还知道存在同构 Id: M1 ~> M1。由于 M1 是初始代数，所以它到另一个代数（包括它自身）只有一个同态。因此前面提到的从 M1 到它自身的两个同态是相同的：H21 ・ H12 = Id，同理有 H12 ・ H21 = Id。因此 H12（和 H21）实际上是同构。 $\blacksquare{}$
这个证明依赖于「从初始代数出发的同态具有唯一性」这一点，即所谓的万有性质（universal property）。在 Jacobs 和 Rutten 的教程中，他们展示了更多利用代数初始性构造的证明。他们认为，这些证明往往比相应的归纳法证明更直观。
定理. 与初始代数同构的代数也是初始代数。
证明. 用同态组合定理易证。 $\blacksquare{}$
语法与语义
字代数的构造给人感觉像一种对函数符号的无脑堆砌，非常的「语法式」。这正是 Gougen 等人（1977）文中的重点，他们在文中提议：将签名 $Σ$ 视作语言的文法规则，将初始 $Σ$-代数 S 视作语言的抽象语法（abstract syntax），将其他的 $Σ$-代数 A 视作语言的语义。
The semantic function is the uniquely determined homomorphism
hA : S ~> A, assigning a meaninghA(s)inAto each syntactic structures in S.
译：语义函数是唯一确定的同态hA : S ~> A，该函数为S中所有的语法结构s赋予其在A中的含义：hA(s)。
即「为语言中的所有项赋予意义」。「相同签名的初始代数之间相互同构」这一点更强化了它作为「抽象语法」的地位：抽象语法可能有很多种表示法，但是这些表示法「本质上相同」。
在我们之前的样例中，NAT 是一个关于自然数及其加法的微型语言的语法；TFc 是这一语言中的项构成的集合（TFN 和 TFCsample 就是这种项的示例）；而其他 NAT-代数则为语言提供了解释，或者说语义：NatUL 是一进制数字语义，NatBool 是奇偶性语义。
From this viewpoint it becomes clear that a major aspect of formal semantics (both practical and theoretical) is constructing intended semantic algebras for particular programming languages.
译：这一角度来看，形式语义（无论是实践还是理论）的一个主要方面显然是：为特定编程语言构造预期的语义代数。（Gougen 等人，1977）
tagless-final 将这一论点作为指导思想，并坚定不移地实践之。当我们确定了签名，就可以立即编写形如 TFN 的语言项。而签名的实现模块则提供了这些语言的解释器，即语义。例如，当我们将 NatUL 模块作为 TFN functor 的参数应用之时，就相当于对 TFN 项进行解释，或者相当于计算其 NatUL-语义。
事实上，像 NatUL 这样定义了一个 NAT-代数（及其载体和运算）的模块，也可以视作「实现了一个用于解释形如 TFN 的 tagless-final 项的解释器」——即构造了一个从 TFC 起始的同态。「代数」就是由「它自己与字代数之间的同态」定义的。编写 tagless-final 解释器就是在定义一个代数，反之亦然。
代数数据类型
现在考虑另一个代数
module ADT = struct
type nat = Z | S of nat | P of nat * nat
let zero = Z
let succ x = S x
let plus (x, y) = P (x, y)
end
正如我们在 tagless-final 方法中所见，ADT 是一个从 TFC 发出的同态。此外，从 TFc 到数据类型 ADT.nat 的映射是单射和满射。因此，这个映射是一个同构，而且 ADT 也是一个初始代数。
练习 7. 找出 ADT 到 TFC 的同态，该同态必然存在。
尽管 TFC 和 ADT 互相同构，即「本质上相同」，但它们之间仍可能存在有用的表示差异。毕竟，对所有相同输入产生相同输出的两个程序也是「本质上相同」的。但我们仍可能有很多理由去偏爱其中一个：这个程序可能更快、更小、是用我们熟悉的语言编写的，或者更易于维护和扩展，等等。
上下文无关文法：多类别代数的一个缩影
上下文无关文法（Context Free Grammar, CFG）是多类别代数的一个典型案例，Gougen 等人（1977，第 3.1 节）中已对其进行了描述。有别于 Gougen 等人中的泛泛而谈，我们使用一个具体的 CFG 例子，和编程语言符号来解释。
考虑下面的 CFG，它涵盖了英语的一个小子集：
S -> NP VP DET -> the
NP -> DET N N -> cat
VP -> TV NP N -> mouse
TV -> TV CTV TV -> chased
CTV -> CRD TV TV -> caught
CRD -> and
非终结符大写，终结符小写。该文法正是 Chomsky 范式（Chomsky Normal Form, CNF）：每个语句都有 NONTERM -> NONTERM NONTERM 或 NONTERM -> term 两种形式（稍后，Chomsky 范式将帮助我们建立 CFG 和 AB 文法之间的联系。它还有助于代数表达变得更清晰）。在这种形式下，文法的生成部分将分为两类：上图左侧的「规则」部分和上图右侧的「词典」部分。顺带一提，每个 CFG 都可以转换成等价的（在生成/识别相同语言意义上的）CNF 文法。
上下文无关文法可被视为用于生成语言的规则集合：即一个「字符串」集合，集合中的每个字符串都是文法中的终结符构成的序列。事实上，每个非终结符都会生成它自己特定的语言。试举一例：我们的文法中的非终结符 NP 只会生成两个字符串：「the cat」以及「the mouse」（为了便于阅读，我们用空格分隔终结符）。另一方面，S 能生成的语言则是无限的，包含了形如「the cat chased the mouse」或「the cat chased and chased and caught the mouse」等字符串。每条文法生成规则都可以解释为「生成对应语言中的字符串」
N -> cat生成了N语言中的「cat」字符串。NP -> DET N则代表了一种字符串，这些字符串由一个DET语言中的任意字符串，以及一个N语言中的任意字符串组成。
从这个角度看，我们不但有对象集合（属于某语言的字符串集合），还有定义在这些集合之上的运算——这与 Birkhoff 对代数的原初定义非常相似。不过，我们可以观察到不只一个载体集合，而是有多个集合：每个「类别」（即语法的非终结符）都有自己的集合。这样，我们就有了一个多类别代数。
我们上面的例子的代数签名如下所示（以 OCaml 模块签名的形式书写）
module type CATMOUSE = sig
type s type vp
type np type tv
type n type ctv
type det type crd
val prod1 : np * vp -> s val the : det
val prod2 : det * n -> np val cat : n
val prod3 : tv * np -> vp val mouse : n
val prod4 : tv * ctv -> tv val chased : tv
val prod5 : crd * tv -> ctv val caught : tv
val and_ : crd
end
（鉴于 and 是 OCaml 中的保留字，这里写成 and_。）与前面的 NAT 签名例子不同，我们可以清楚的看到有许多类别——事实上有 8 种，与语法中的非终结符一一对应。这个签名看起来与文法定义惊人地相似，不过是交换了规则的两侧，这种紧密的对应关系正是 Chomsky 范式的独特优势。唯一显著的变化是：在模块定义中，我们为文法规则添加了形如 prod1 的名称。给规则命名通常很有用，但传统的 CFG 记法往往缺少这种命名，而在 CFG 的代数表达中，为其命名是不可避免的。另一个值得注意的地方是：文法中的每个终结符在代数中都被视为一个零参运算。
CATMOUSE 签名的一个代数是字符串代数：
module CMString = struct
type s = string type vp = string
type np = string type tv = string
type n = string type ctv = string
type det = string type crd = string
let ccat : string * string -> string = fun (x,y) -> x ^ " " ^ y
let prod1 = ccat let the = "the"
let prod2 = ccat let cat = "cat"
let prod3 = ccat let mouse = "mouse"
let prod4 = ccat let chased = "chased"
let prod5 = ccat let caught = "caught"
let and_ = "and"
end
每个非终结符都代表了一个字符串集合，即一种语言。换言之，某类别的载体集合（如 vp）就是起始符为 VP 的文法所生成的语言。
练习 8. CMString 是初始代数吗？
练习 9. 我们可以认为 CMString 代数实现了「将上下文无关文法用作生成语言的规则集合」这一观点。然而，CMString 只展示了如何生成语言中的一个字符串：例如，prod1 告诉我们如何从 NP 和 VP 语言的字符串生成 S 语言的字符串。请使用 CMString 编写一个程序，这个程序能生成 NP、VP、S 等语言的所有字符串。
有人可能会问：「CATMOUSE 签名的 TFC（见「初始代数」一节）类似物是什么？」它应是一个多类别代数：我们不妨称之为 TFCATMOUSE，它应具有 s，np，vp 等类别。而其类别（以 np 为例）的载体集合是一个类型为 TFCM_np 的 OCaml functor 集合。
module type TFCM_np = functor(CM: CATMOUSE) -> sig val e : CM.np end
module type TFCM_s = functor(CM: CATMOUSE) -> sig val e : CM.s end
同理，签名上的类别 s 的载体集合均应为对应 TFCM_s 类型的 functor 集合。下面是这些载体集合的几个典型元素：
module TFcm_thecat(CM: CATMOUSE) = struct
open CM
let e = prod2 (the, cat)
end
module TFcm_chase(CM:CATMOUSE) = struct
open CM
let e =
prod1(prod2(the,cat),
prod3( prod4(chased, prod5(and_, prod4(chased, prod5(and_, caught)))),
prod2 (the,mouse)))
end
这些 functor 均以前述 TFN 的方式构建。
练习 10. 以 TFC 为例，将 TFCATMOUSE 明确写成一个 OCaml 模块。
练习 11. 再以 TFC 为例，证明 TFCATMOUSE 是一个初始代数。作为这一证明的前提条件，先证明 TFCATMOUSE 上的所有类别的载体集合都非空。
让我们仔细观察 TFCATMOUSE 上载体集合的元素。以 TFcm_chase 为例，像 TFcm_chase.e 这样的项是仅使用代数上的常量和运算构造的。在 CFG 的术语中，这种项展示了 CFG 生成规则的一种特定应用：TFcm_chase.e 表示 CATMOUSE 语法的分析树（parse tree）（或派生树）。如果我们将 TFcm_chase 模块输入 OCaml，会发现类型检查器接受了这个项。这意味着 TFcm_chase.e 是良类型的，它代表了一次合法的 CFG 生成规则应用——或者说，它代表了一颗合法的分析树。
因此，我们得出了 Gougen 等人（1977）中的结论：对于表示某 CFG 的代数签名，其初始代数的载体集合代表「文法从每个非终结符中派生而出的分析树」。
此外，如果我们以 TFcm_chase 的方式编写初始代数或其载体集合中的元素，那么文法派生（或分析树）的合法性可以通过 OCaml 类型检查器进行机械检查。
鉴于 TFCATMOUSE 是一个初始代数，因此它与其他具有相同签名的代数（如 CMString）之间存在唯一的同态关系。这一同态可以将 TFCATMOUSE 的载体元素映射成 CMString 的载体元素（即字符串），如：
let module M = TFcm_chase(CMString) in M.e
- : string = the cat chased and chased and caught the mouse
（缩进行展示了求值结果）换言之，从 TFCATMOUSE 到 CMString 的同态其实计算的是——该分析树派生出的字符串。
练习 12. 从 TFCATMOUSE 到 CMString 的同态是单射吗？是满射吗？这一同态的单射性质与文法的二义性（ambiguty）有什么关系？
Gougen 等人（1977）文中概括道：若 G 是某 CFG 文法，TG 是该文法对应的签名的初始代数，那么任何具有相同签名的代数 S 都能为 G 生成的上下文无关语言提供语义。
TG, being initial, gives the unique homomorphismhs : TG ~> Swhich assigns`meanings'' inSto all syntactically well-formed phrases of the language. 译：TG具有初始性，它为我们提供了到任意S的唯一同态hs : TG ~> S，这一同态确保了语言中所有形式良好的的语句都能在S` 中被赋予「意义」。
练习 13. 在 Gougen 等人（1977）中，作为进一步的例子，他们概述了如何将 Knuth 的属性文法（attribute grammar）视为一种「为 CFG 派生赋予意义的代数」（他们还指出「但 Knuth 的定义和记号看起来比所必须的还要复杂」）。这些代数的载体集合是由元组构成的集合：即合成属性（synthesized attribute）（继承属性（inherited attribute）需要更详细的说明）。试着思考 CATMOUSE 的属性文法，并将这一文法作为 CATMOUSE-代数来实现。
最后，经典的指称语义（denotation semantics）不过是 CFG 初始代数解释的又一个样例。Gougen 等人指出：Scott 的《Data types as lattices》肇始于「将 BNF 扩展到语义」这一思想。Scott 和 Strachey 在《Towards a mathmatical semantics for computer languages》中写道：
The semantical definition is syntax directed in that it follows the same order of clauses and transforms each language construct into the intended operations on the meanings of the parts.
译：语义定义是语法导向的：它遵守和语法相同的子句顺序，并将每个语言构造转换为对各部分的意义的预期运算。
Gougen 等人点评之：
This essentially says that syntax is context-free and semantics is a homomorphism.
译：这本质上是在说：语法是上下文无关的，而语义是一个同态。
参考
译者注：Joseph Gougen 还指导设计了 OBJ 语言，该语言中也大量使用了类似 OCaml 模块的抽象设施。 ↩︎