Algebraic theories 笔记 ⬝ Zero Calorie Drink Shop

Andrej Bauer 的 Lecture 1 的笔记。

视频和资料：https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#Bauer

简介：本次讲座介绍数学（Algebraic theories），可参考文章 What is algebraic about algebraic effects and handlers? 的第 1 节

first of all let’s start from group as an example.

Example: a group: $(G, u, \cdot, ^{-1})$ - this is the operation

and equations: $u \cdot x = x = x \cdot u$ , $(x \cdot y) \cdot z = x \cdot (y \cdot z)$ and $x \cdot x^{-1} = u = x^{-1} \cdot x$

alternative: a monoid: $(M, u, \cdot)$ - this is the operation

operations and equations are important.

signature and operations

Definition: A signature $\Sigma = \{(op_i, N_i)\}_{i \in I}$ where $op_i$ are operation symbols 一个 op 和一个自然数 as argument

Definition: a term in context $x_i, ..., x_n$ is

one of the variables $x_i$
or $op_i$ applied to some terms, $op_i(t_1, t_2, ...)$ where the terms are in context

↑ read as inductive definition

Def: an algebraic equational theory T is $\Sigma_T, \epsilon_T$ where $\Sigma_T$ is signature and $\epsilon_T$ is a set of equations

an equation is

…

Example of group:

sig: $\Sigma_{group} = \{(u, 0), ( \cdot , 2), (^{-1}, 1)\}$

for typing convenience we write down $\cdot$ as cdot, $^{-1}$ as inv

so, equations is:

x | cdot (u(), x) = x
x | cdot (x, inv(x)) = x

Example of a semilattice

sig: {(bottom, 0), (join, 2) eq:

(x join y) join z = x join (y join z)
bottom join x = x
x join y = y join x
x join x = x

so far we described a piece of formalism

let’s introduce the language of algebra theory

suppose $T$ a theory (algebraic)

an interpretation $I$ of $\Sigma_T$ is given by

a carrier set $|I|$
a bunch of maps $(op_i, n_i) \in \Sigma_T$ $(o p_{i}, n_{i}) \in Σ_{T}$ :
- $⟦ op_i ⟧_I: |I| \times ... \times |I| \rightarrow |I|$ （args 有 $n_i$ 个 $|I|$ ）

we write $⟦ x ⟧$ as interpretation

each term $x_1, ..., x_k | t$ is interpreted as a map $⟦ x_1, ..., x_k | t ⟧: |I|^k \rightarrow |I|$

follows:

$x_i$ is i-th projection
$⟦ x_1, ..., x_k | op_i (t_1, t..., t_{n_i}) ⟧$ is a composition:

$|I|^k \rightarrow |I|^{n_i} \rightarrow |I|$ where the first arrow uses $⟦ t_1⟧, ⟦t_2⟧, ... ⟦t_{n_i}⟧$ and the second arrow uses $⟦ op_i ⟧$

Def: A $T$ -model is an interpretation M of theory T s.t. for every

$x_1, ..., x_k | l = r$ in $\epsilon_T$

the maps:

$⟦ x_1, ... x_k | l ⟧_M: M^k \rightarrow M$
$⟦ x_1, ... x_k | r ⟧_M: M^k \rightarrow M$

…

Example: a model $M$ of the theory of a pointed set:

a carrier set $|M|$
a map $⟦ \cdot ⟧_M$ : $|M^0| \rightarrow M$

Example: every theory T has the trivial model M:

|M| = 1
⟦ op_i ⟧_M: 1^n_i \rightarrow 1

field is not algebraic. why: gpt:

你问到的是一个很容易让人混淆但其实很深刻的点：为什么在 algebraic theory（代数理论） 的语境下，field（域）不是“algebraic”的，而像 $\mathbb{Z}\_2 \times \mathbb{Z}\_3$ 这种例子会被拿来说明问题。

我帮你把这个逻辑拆开讲清楚👇

🧠 核心一句话

👉 在这里，“algebraic”指的是： 能用“有限个运算 + 等式公理”完全描述的结构（equational / algebraic theory）

而 field 做不到这一点。

1️⃣ 什么叫 “algebraic theory”？

在这个语境里，它的意思是：

👉 只允许用：

运算（+、× 这种函数）
等式（=）

来写公理

比如：

✅ 群（group）是 algebraic 的

公理是：

( (xy)z = x(yz) )
( e*x = x )
( x^{-1} * x = e )

👉 全是“等式”，没有条件判断

2️⃣ field 哪里出问题？

域的关键公理是： $x \neq 0 \Rightarrow \exists y,; x \cdot y = 1$

问题在这里👇

👉 这不是“纯等式” 而是：

有条件（(x ≠ 0)）
有存在量词（∃）

🚫 algebraic theory 不允许：

❌ “如果……那么……”（条件）
❌ “存在一个……”（∃）

它只能写： $\text{某个表达式} = \text{另一个表达式}$

3️⃣ 直觉理解

algebraic theory 像什么？

👉 “盲算规则机器”

只能说：

怎么算
算出来必须相等

不能说：

“如果 x ≠ 0 才能怎样”

4️⃣ 为什么拿 $\mathbb{Z}_2 \times \mathbb{Z}_3$ 举例？

我们写成： $\mathbb{Z}_2 \times \mathbb{Z}_3$

这个结构：

是两个域的“直积”
运算是分量计算

✨ 关键性质

在 algebraic theory 里：

👉 如果一个结构满足某些等式公理，那么它的直积也满足

举个例子

如果“field”是 algebraic 的，那么：

$\mathbb{Z}\_2$ 是 field ✅
$\mathbb{Z}\_3$ 是 field ✅

👉 那么它们的直积也必须是 field ❗

💥 但现实是： $(1,0) \neq 0$

但它没有逆元： $(1,0) \cdot (x,y) = (1,0)$

永远不可能等于 ((1,1))

👉 所以：

❌ 它不是 field

🎯 这说明了什么？

👉 “field 的性质无法只用等式表达”

因为：

等式公理会“自动传递”到直积
但 field 的性质不会

5️⃣ 本质总结

algebraic structure（代数结构）

只用等式描述
对直积封闭

field

需要：
- 条件（(x ≠ 0)）
- 存在性（∃逆元）
❌ 不是纯等式结构

🧠 更深一层（你可能会喜欢这个）

其实 field 是：

👉 first-order theory（一级逻辑） 而不是： 👉 equational theory（等式理论）

🌟 一句话总结

👉 field 之所以不是 algebraic 的，是因为“可除性”无法用纯等式表达，而必须用条件和存在性，这破坏了 algebraic theory 的封闭性（尤其是对直积）。

如果你愿意，我可以再往下讲一个很有意思的点：

👉 为什么“存在逆元”这种东西，本质上就是“不可代数化”的？（和程序里的 pattern matching / partial function 很像）

free model

这个问题问得很到点子上了，因为 **free model（自由模型）**基本就是 algebraic theory 里的“核心构造”。我们一步一步把它讲清楚，而且尽量贴直觉。

🧠 一句话直觉

👉 free model = 在不引入任何“额外关系”的前提下，由一组生成元“自由生成”的最一般结构

或者更程序员一点：

👉 就是“只按语法构造出来的结构”，没有任何额外约束

1️⃣ 在 algebraic theory 里的背景

我们说一个 theory 是 algebraic 的，意思是：

有一些运算（比如 (+), $\cdot$ ）
有一些等式公理（比如结合律）

👉 一个 model（模型） = 一个具体实现这些运算并满足公理的结构

比如：

群的一个 model = 某个具体群
环的一个 model = 某个具体环

2️⃣ free model 是什么？

给你一个集合 (X)（叫生成元 generators）

👉 free model on (X) 满足：

✅ 条件 1：包含这些生成元

有一个映射： $\eta: X \to F(X)$

✅ 条件 2（最关键！）：通用性质（universal property）

对于任何 model (A)，以及任意函数： $f: X \to A$

都存在唯一一个结构保持映射（homomorphism）： $\tilde{f}: F(X) \to A$

使得： $\tilde{f} \circ \eta = f$

🧠 翻译成人话

👉 你只要告诉我：

每个 generator 要变成什么

👉 free model 就会：

自动帮你扩展成整个结构
而且是唯一的

3️⃣ 最经典例子

🟢 自由群（free group）

给定生成元集合 (X = {a,b})

👉 free group 就是：

所有由 (a, b) 和它们的逆组成的“字符串”
只允许用群公理化简（比如 (aa^{-1} = e)）

但：

👉 没有额外关系

不会强行规定 (ab = ba)

🟢 自由幺半群（free monoid）

👉 就是所有字符串： $X^*$

运算 = 拼接
单位元 = 空串

🟢 自由环 / 自由代数

👉 就是“多项式”，但变量之间没有关系

比如： $\mathbb{Z}\langle x, y \rangle$

4️⃣ 为什么叫 “free”？

👉 因为它是：

最不受约束的
只满足公理，没有额外关系

5️⃣ 和你刚才的问题的联系（关键 insight）

你前面问：

为什么 field 不是 algebraic 的？

现在可以看出一个关键点👇

algebraic theory 的一个特征：

👉 一定存在 free models

但 field 呢？

如果你尝试构造：

👉 “free field on X”

会出问题：

你必须允许除法
但不能除以 0
这不是纯 equational 的

👉 结果：

构造非常复杂（要做分式域、再 quotient）
不再是“语法自由生成”

6️⃣ 更抽象一点（但很重要）

free model 本质上是：

👉 一个 left adjoint（左伴随） $F : \text{Set} \to \text{Model}$

它的意义是：

👉 “从集合生成最自由的结构”

7️⃣ 一个非常直观的类比

你可以这样理解：

free model = AST（抽象语法树）

比如你有：

常量：(a, b)
运算：(+)

👉 free model 就是：

a
b
a + b
(a + b) + a
...

然后：

👉 其他 model = “解释器”

把这些表达式解释成：

数字
矩阵
函数

🌟 总结一句话

👉 free model 是“由生成元构造的、只满足公理、不引入额外关系的最一般模型”，它的本质是一个具有通用性质的“语法结构”。

如果你愿意，我可以再讲一个更深的点（会很有意思）：

👉 为什么 free model 本质上就是“程序语法”，而 algebraic theory ≈ “可解释的编程语言”？

为什么 every algebraic theory has a free model

这个结论其实可以说成一个更精确的版本：

👉 对任何 algebraic theory（等式理论），都有一个“自由模型构造” (F(X))，对任意集合 (X) 都存在。

你问“为什么一定存在”，核心原因其实是：

👉 因为 algebraic theory 只用“运算 + 等式”，所以可以用“语法项（terms）”直接构造一个模型。

我们一步一步拆开讲。

🧠 1️⃣ 核心直觉

👉 algebraic theory 的一切东西，本质都是：

一些运算符（signature）
一些等式规则（equations）

那么你自然可以做一件事：

👉 把所有“合法表达式”都写出来

这就已经是一个候选模型了。

✨ 2️⃣ 构造方法（这就是为什么一定存在）

给定：

一个 algebraic theory (T)
一个生成元集合 (X)

我们这样构造 free model (F(X))：

第一步：生成所有“语法项”（terms）

比如：

$x \in X$
如果有运算 (+)，就可以构造：
- (x + y)
- ((x + y) + z)
- …

👉 得到一个巨大集合：Term(X)

第二步：按公理“取商”（quotient）

如果 theory 里有公理： $(x + y) + z = x + (y + z)$

👉 那我们就把这些表达式“视为相等”

于是得到： $F(X) = \text{Term}(X) / \sim$

第三步：定义运算

运算直接在表达式上做： $[a] + [b] := [a + b]$

👉 自动是良定义的（因为我们已经 quotient 了）

🎯 这一步就是关键

👉 整个构造只用了：

语法生成
等式识别（quotient）

👉 没有用到：

条件（if）
存在性（∃）

🧠 3️⃣ 为什么这保证“一定存在”？

因为：

👉 这个构造是纯组合性的（syntactic）

语法树一定能生成
等价关系一定能取商

👉 所以 free model 可以机械地构造出来

💥 对比：为什么 field 不行

回忆 field 的关键公理： $x \neq 0 \Rightarrow \exists y,; xy = 1$

你没法用“语法项 + 等式”来表达：

“x ≠ 0”
“存在 y”

👉 所以你不能：

只靠“表达式”构造一个 free field

结果是：

👉 free field 不再是简单的 term algebra 而是要做：

分式
等价类
排除非法情况

👉 构造变得非语法化

🧩 4️⃣ 更高层解释（范畴论视角）

对于 algebraic theory：

👉 有一个忘却函子： $U: \text{Model} \to \text{Set}$

（把模型忘掉结构，只看底层集合）

关键定理：

👉 这个函子一定有左伴随： $F: \text{Set} \to \text{Model}$

这就是 free model。

为什么一定有？

因为：

👉 algebraic theory 本质上就是：

一个 finitary monad
或 Lawvere theory

而这些结构保证：

👉 自由代数一定存在

🧠 5️⃣ 再用程序类比一次（非常本质）

你可以这样理解：

algebraic theory ≈ 编程语言语法

运算 = 函数符号
公理 = rewrite rules

free model = AST（抽象语法树）

👉 永远可以构造 AST：

Add(Add(x, y), z)

然后再按规则化简。

👉 所以 free model 一定存在，本质原因是：

语法总是可以自由生成

🌟 最终总结

👉 每个 algebraic theory 都有 free model，是因为它的公理是纯等式的，这允许我们用“语法项 + 等价关系”直接构造一个模型，这个构造是完全机械且总是可行的。

如果你想再深入一步，我可以讲一个很关键的桥梁：

👉 为什么“free model 存在”其实等价于“这个理论是 monadic 的”？（这会把 universal algebra 和 category theory 连起来）

其实我没看懂什么是一个 model

很好，这一步卡住是非常正常的——因为“model”这个词本身就有点抽象。我们换一个更直观 + 分层的方式来讲，让你真正“抓住它”。

🧠 一句话直觉

👉 model（模型）= 把一套“符号规则”真正变成“具体东西”的实现

1️⃣ 从最简单的例子开始

假设我写一个“理论”（theory）：

有一个运算：(+)
满足规则： $x + y = y + x$

👉 这只是“规则”，还没有具体对象

什么是 model？

👉 一个 model 就是：

给你一个具体集合
告诉你 (+) 到底怎么计算
并且满足这些规则

举例

✅ 这是一个 model

集合：整数 $\mathbb{Z}$

运算：普通加法

✔ 满足交换律

✅ 这也是一个 model

集合：二维向量

运算：向量加法

✔ 也满足交换律

👉 它们都是“同一个理论”的不同实现

🎯 关键理解

👉 theory 是“语法规则” 👉 model 是“具体解释”

2️⃣ 一个更程序员的类比（非常重要）

你可以这样理解：

theory = 接口 / 抽象类

interface Addable {
  add(x, y): T;
  // 要满足：add(x,y) == add(y,x)
}

model = 一个具体实现

class IntegerAdd implements Addable {
  add(x, y) = x + y
}

或者：

class VectorAdd implements Addable {
  add(x, y) = vector_add(x, y)
}

👉 这些实现就是 models

3️⃣ 回到 algebraic theory 的语境

一个 algebraic theory 包含：

一些运算符（signature）
一些等式（equations）

model =

👉 一个集合 (A)，加上：

每个运算符的具体实现（函数）
满足所有等式

4️⃣ 再举一个更“代数味”的例子

群（group）这个 theory

它说：

有运算 (*)
有单位元 (e)
有逆元
满足结合律

model 就是：

任何一个具体群，比如：

整数加法群 ( $\mathbb{Z}, +$ )
非零实数乘法群
置换群

👉 每一个“具体群” = 一个 model

5️⃣ 为什么叫 “model”？

这个词来自逻辑学：

👉 意思是：

“让这些公式为真”的东西

比如： $x + y = y + x$

👉 在整数里是真的 ✔ 👉 在矩阵乘法里不是真的 ❌

所以：

整数是这个 theory 的 model
矩阵乘法不是

🧠 6️⃣ 一点点更抽象（但很关键）

你可以这样统一理解：

theory

= 一堆符号 + 规则（纯语法）

model

= 一个“解释函数”，把：

符号 → 具体运算
变量 → 具体元素

并让所有规则成立

🔥 7️⃣ 和 free model 的关系

现在你可以理解这句话了：

👉 free model 是一种“最通用的 model”

它的特点是：

元素 = 纯表达式（语法树）
没有额外关系
任何其他 model 都是它的“解释”

🌟 最终总结

👉 model 就是：一个具体世界，在这个世界里，你的理论规则都成立。

如果你愿意，我们可以继续往前推进一个非常关键的点（会让你彻底通）：

👉 为什么“model = 解释”，而“free model = 语法本身”？（这其实是整个 universal algebra / type theory 的核心桥梁）

解释这个板书（懒得放板书图片）

很好，这张板书其实已经把 “algebraic = 语法 + 等式” 讲得非常本质了，只是写法比较“范畴/PL风”，我们把它逐行翻译成人话。

🧠 整体在干嘛？

这段在做一件事：

👉 构造 free model（自由模型）

并且用的是：

👉 “语法树（syntax tree）”的方式来构造

这正是“algebraic”的核心： 一切从语法出发

🧩 上半部分：Term in context

板书：

Term in context (x_1, …, x_k) is:

one of the variables (x_i)

(op_i(t_1, …, t_n)) where (t_1,…,t_n) are terms

👉 翻译

在变量集合 (x_1,…,x_k) 下，一个 term（表达式）可以是：

1️⃣ 一个变量

比如：

x₁

2️⃣ 一个运算应用

op_i(t₁, ..., tₙ)

其中：

(op_i)：某个操作（operation）
(t₁,…,tₙ)：已经是 term 的东西

🧠 关键点

👉 这是一个归纳定义（inductive definition）

也就是：

从最简单的（变量）开始
不断用运算“长出更复杂的表达式”

✨ 直觉

这就是在定义：

👉 所有“合法程序 / 表达式”的集合

🌳 下半部分：Free model = Tree_T(X)

板书：

Free model (Free_T(X)):

(Tree_T(X)) = set of well-founded trees, defined inductively

👉 翻译

自由模型就是：

👉 所有“良基树”（well-founded trees）组成的集合

什么是 tree？

比如一个表达式：

op(a, op(b, c))

可以画成：

      op
     /  \
    a   op
        / \
       b   c

👉 这就是一棵树

“well-founded” 是啥？

👉 没有无限向下的结构

也就是：

不会有无限展开
每个表达式都是有限的

👉 本质就是：有限语法树

🧩 具体构造规则

板书：

规则 1：

for every (x ∈ X), there is tree return (x ∈ Tree_T(X))

👉 每个变量本身就是一棵树

规则 2：

if ((op_i : n_i) ∈ Σ_T) and (t₁,…,tₙ ∈ Free_T(X))

👉 如果：

有一个操作 (op_i)，参数个数是 (n_i)
已经有 (n_i) 个子树

then (op_i(t₁,…,tₙ))

👉 那就可以构造一棵新树：

        op_i
       / ... \
     t₁      tₙ

🎯 这整个构造在干嘛？

👉 在构造：

👉 所有可能的“语法表达式”

也就是：

term algebra（项代数）

🔥 关键 insight（这就是 algebraic 的本质）

现在你可以理解老师想表达的核心了：

👉 algebraic = 可以用“语法树”构造 free model

因为：

运算 = 语法构造规则
公理 = 等式（之后再 quotient）

👉 free model = “纯语法世界”

里面的元素就是：

x
op(x,y)
op(op(x,y), z)
...

👉 没有任何“解释”（interpretation）

🧠 和 model 的关系（关键桥梁）

现在你可以把三件事连起来：

1️⃣ free model

= 所有语法树

2️⃣ 一个 model（比如整数）

= 给这些语法一个“解释”

比如：

op = +
x = 3
y = 5

👉 那：

op(x,y) → 8

3️⃣ homomorphism

就是：

👉 把“语法树”映射到“具体值”

💥 为什么这说明 “field 不是 algebraic”

因为这里的构造：

👉 完全是语法驱动的

你只需要：

运算符
参数个数

但 field 需要：

“x ≠ 0 才能除”
“存在逆元”

👉 这些不是语法能表达的

🌟 一句话总结这块板书

👉 这段板书在说明：algebraic theory 的 free model 可以用“语法树（term trees）”归纳地构造出来，而这正是 algebraic 的本质——结构完全由运算的语法生成。

🧠 如果再往前一步（非常关键）

这其实就是 PL 里的一个巨大对应关系：

概念	对应
algebraic theory	语言语法
term	AST
free model	所有程序
model	解释器
homomorphism	解释过程

如果你愿意，我可以帮你把这个直接连到：

👉 algebraic effects 为什么“必须是 algebraic”的（那一步会直接通整个 PL 语义）