逻辑

#logic @ 2026-08-14T07:51:52+08:00

Lawvere’s Fixed-point Theorem

Lawvere’s Fixed-point Theorem: 令 $𝐶$ 是一个 Cartesian closed category， $𝐴, 𝐵 \in ob (𝐶)$ ，如果存在 $𝑓 : 𝐴 \to 𝐵^{𝐴}$ weakly point-surjective，那么 $𝐵$ 上的任何自态射都有不动点。

Weakly point-surjective: CCC 中 $𝑓 : 𝑋 \to 𝑍^{𝑌}$ weakly point-surjective iff. 对于任意 $𝑔 : 𝑌 \to 𝑍$ ，存在 $𝑥 : 𝟏 \to 𝑋$ 使得 $𝑓 \circ 𝑥$ 和 $𝑔$ Pointwise 相等，即对任意 $𝑦 : 𝟏 \to 𝑌$ ，都有 $𝑔 \circ 𝑦 = eval (𝑓 \circ 𝑥, 𝑦)$

不动点: $𝑔 : 𝐵 \to 𝐵$ 上有不动点指存在一个 $𝑏 : 𝟏 \to 𝐵$ ，使得 $𝑏 = 𝑔 \circ 𝑏$

Proof:
对于任意 $𝑔 : 𝐵 \to 𝐵$ ，定义 $ℎ : 𝐴 \to 𝐵 ≝ 𝑔 \circ eval \circ (𝑓, id)$ _{[ $ℎ (𝑥) = 𝑔 (𝑓 (𝑥, 𝑥))$ ]}
因为 $𝑓$ Weakly point-surjective，存在 $𝑎 : 𝟏 \to 𝐴$ “represents” $ℎ$ ，那么令 $𝑏 = eval \circ (𝑓 \circ 𝑎, 𝑎)$ _{[ $𝑏 = 𝑓 (𝑎, 𝑎)$ ]}：
$𝑔 \circ 𝑏 = 𝑔 \circ eval \circ (𝑓 \circ 𝑎, 𝑎) = ℎ \circ 𝑎 = eval (𝑓 \circ 𝑎, 𝑎) = 𝑏$

Lawvere’s Fixed-point Theorem 通常被认为是数个对角化方法的统一。常见使用的路径有两个：

选择一个显然没有不动点的自态射（比如 $\neg : Ω \to Ω$ ），然后构造 Weakly point-surjectivity，产生矛盾。
通过 Weakly point-surjective 态射证明存在不动点。

比较常见的三个例子。可以看到，其实很多时候直接上 Lawvere’s Fixed-point Theorem 其实不是很好用…

Cantor’s proof of $𝒫︀ (𝐴) > 𝐴$

$𝐒𝐞𝐭$ 里面的 Subobject classifier $Ω$ 就是布尔值 $𝟐$ , $\neg : 𝟐 \to 𝟐$ 没有不动点。 $𝒫︀ (𝐴) ≃ 𝟐^{𝐴}$ 。如果 $𝒫︀ (𝐴) \leq 𝐴$ ，即存在 $𝑓 : 𝐴 \to 𝟐^{𝐴}$ 是 Weakly point-surjective 的，立刻得到矛盾。

Turing’s Halting problem

范畴选择为：

对象是所有 $ℕ$ 上的 partial equivalence relation (PER)
态射是等价类之间的 Total computable 函数。强调这里需要是 Total 的，因为 Partial halting recognizer 显然存在（就是 UTM）。一个额外的限制是，因为我们的对象是 PER，需要这里要求每个态射在同一个等价类内的输入上的输出都等价。_{[最严格的说法：态射是商集 Field(R)/R -> Field(S)/S 之间、由在 Field(R) 上全定义的部分可计算函数跟踪的函数。]}

CCC 结构：

Terminal object 是 ${0}$
Product 是 Tuple 在图灵机输入上的编码
Exponential object 是图灵机的编码, quotient by 函数外延性（在所有输入上输出都等价的图灵机被 Quotient 到一起）, eval 是 UTM。因为我们商掉的关系是函数外延性，所以这里 eval 是一个良定义的态射。

这里需要 Argue 一下 eval 也是 Total 的。注意到因为 Exponential object 里只包含 Total Turing machine 的编码，所以 eval externally 可以看到一定是停机的。

接下来 Abuse 两个记号： $𝟐 = ({0, 1}, =)$ 是布尔值, $(ℕ, =)$ 直接写作 $ℕ$ 。

使用 $𝟐$ 表示是否停机。假设存在 Total halting decider $ℎ : ℕ \to 𝟐^{ℕ}$ （或者 $ℕ \times ℕ \to 𝟐$ , 注意到图灵机可以 Curry，这两个东西就是一样的），其中：

如果 $𝑥$ 不是一个合法的图灵机编码， $ℎ (𝑥)$ 是一个恒为 0 的函数。编码检查是可判定的。
如果 $𝑥$ 是一个合法的图灵机编码，不一定 Total， $ℎ (𝑥) (𝑦)$ 输出 0 当且仅当 $𝑥$ 对应的图灵机在输入 $𝑦$ 时停机。

$ℎ$ 是 Weakly point-surjective 的。对于任意 $𝑔 : ℕ \to 𝟐$ ， $𝑔$ 对应 $ℕ$ 的可判定子集，所以一定存在一个图灵机，当且仅当在这个可判定子集上停机。这个图灵机的编码 weakly represents $𝑔$ 。注意，这个图灵机的编码是在 $ℕ$ 里，不是在 $2^{ℕ}$ 里，所以它可以本身是 Partial 的。

最后， $𝟐$ 上存在 Total computable 函数 $\neg = {0 \mapsto 1, 1 \mapsto 0}$ 没有不动点。所以这样的 $ℎ$ 一定不存在。

Remark: 考虑如下映射：如果输入在 $𝟐^{ℕ}$ 内，那么不变，否则映射到某个特定的输出常数 0 的图灵机。这个映射是 Weakly point-surjective 的，所以也肯定不存在。所以在上述范畴的定义下，一个 Total computable function 可以检查图灵机的编码，但是无法判断一个编码是不是在 $𝟐^{ℕ}$ 内。这是 Totality problem.

Caveats & further remarks

为什么要商一个 PER？

如果不商 PER 的话，问题来自于态射集 $𝑋 \to 𝑌$ 如果定义成 Total computable 函数，那么这是外延的：任意两个行为一样的函数是同一个态射。但是 Exponential object 如果定义成图灵机编码，那么可能有多个不同编码。这违反了 CCC 要求的 Universal property。

如果我们把态射集也定义成内涵的，最大的问题来自于 $id \circ (-)$ 在态射集上会把一个态射映射成另一个不一样的态射。

最后，最简单的办法其实是避开 CCC：根本不用 Exponential object，直接在 $𝐴 \times 𝐴 \to 𝐵$ 上定义 Weakly point-surjectivity。事实上，在下面 Diagonal lemma 的证明中，我们甚至要把 Weakly point-surjectivity 都去掉。

Also see: Effective Topos.

Gödel’s diagonal lemma

Diagonal lemma 用的是第二条路径，构造不动点。

首先，我们要简化一下 Lawvere’s theorem 的证明。注意到如果我们把上面的证明打开，有两个可以简化的地方：

首先，其实根本不用 CCC。直接去表示 $𝐴 \times 𝐴 \to 𝐵$ 中的一个分量就行了。
其实我们也不需要任意自映射都被 represent：上面选到的那几个特定函数能够被表示就行。下面如果我们要构造特定自映射的不动点，只需要找到这个映射本身对应的 $ℎ$ 的 representative 即可。

Local Lawvere’s Lemma: 给定 $𝑔 : 𝐵 \to 𝐵$ 。如果存在 $𝑓 : 𝐴 \times 𝐴 \to 𝐵, 𝑎 : 𝟏 \to 𝐴$ 满足对于任意 $𝑥 : 𝟏 \to 𝐴$ ，都有 $𝑔 \circ 𝑓 \circ (𝑥, 𝑥) = 𝑓 \circ (𝑥, 𝑎)$ ，那么 $𝑓 \circ (𝑎, 𝑎) = 𝑔 \circ 𝑓 \circ (𝑎, 𝑎)$ 是 $𝑔$ 的不动点。

这样做的好处是我们在定义范畴的时候可以放松非常多，并不需要把态射想方设法限制到能表示的那些上了。比如允许我们选用 $𝐒𝐞𝐭$ 作为范畴。同时，注意到 $𝑓$ 甚至可以依赖 $𝑔$ 选择。

选择经典的场景：理论选用 Q， $(-)$ 表示某个整数在语言内对应的表示， $⌜ - ⌝$ 表示编码。对于任意语句 $𝑆$ ， $[𝑆]$ 表示 $𝑆$ 在 Q 内的可证等价语句类。令 $𝐿$ 表示所有这样的等价类构成的集合。

令 $𝐵 = 𝐿 \times ℕ$ ，其中我们关心的元素是某个语句的可证等价类及其编码构成的 Tuple。

对于任意给定的一元谓词 $𝜓 (𝑥)$ ，可以对应一个 $𝐵$ 上的自映射 $𝑔_{𝜓} : (𝑐, 𝑛) \mapsto ([𝜓 (𝑛)], 𝑛)$ 。这个自映射是把第一个分量里的语句等价类改成了 Tuple 第二个分量带有的自然数包上一次 $𝜓$ 。接下来需要找到对应的矩阵 $𝑓$ 可以满足要求的表示条件： $𝑔_{𝜓}$ 作用在矩阵的对角线上被某一列表示。

定义 $𝑑 : ℕ \to ℕ$ :

𝑑 : (⌜ 𝛼 (𝑥) ⌝) \mapsto ⌜ 𝛼 (⌜ 𝛼 (𝑥) ⌝) ⌝

… 其中 $𝛼 (𝑥)$ 不是一个语句，x 是自由变元。我们将其原样做 Gödel coding。对于不是一元谓词编码的输入，输出 0。根据 Gödel coding 可以在 Q 内被表示，存在一个可定义的一元谓词 $𝛾 (𝑥)$ 满足对于任意 $𝑛 \in ℕ$ ,

𝑸 ⊢ 𝛾 (𝑛) \leftrightarrow 𝜓 (𝑑 (𝑛))

直觉： $𝑑$ 表示一次 self-application， $𝛾$ 表示一次 self-application 之后落到 $𝜓$ 里

令 $𝐴$ 表示所有一元谓词集_{[可以多加一点限制，比如变元名称是 x]}。考虑如下 $𝑓 : 𝐴 \times 𝐴 \to 𝐵$ ：

𝑓 (𝛼, 𝛽) = ([𝛽 (⌜ 𝛼 (𝑥) ⌝)], 𝑑 (⌜ 𝛼 (𝑥) ⌝))

注意到，在对角线上， $𝑓 (𝛼, 𝛼) = ([𝛼 (⌜ 𝛼 (𝑥) ⌝)], ⌜ 𝛼 (⌜ 𝛼 (𝑥) ⌝) ⌝)$ 记录的元素正好是一些语句及其可证等价类。所以只需找到 $𝑔_{𝜓}$ 在对角线上的不动点即可。

直觉：
$𝛼$ -行：“ $𝛼$ 被该列描述”，以及 $𝛼$ self-application
$𝛽$ -列：“该行由 $𝛽$ 描述”，及被描述谓词的 self-application
$(𝛼, 𝛽)$ ：“ $𝛽$ 描述 $𝛼$ “，以及 $𝛼$ self-application
$(𝛼, 𝛼)$ : “ $𝛼$ 描述 $𝛼$ “，并且此时第二个分量正好变成前面这句话的 Gödel number

那么：

\begin{aligned} 𝑓 (𝛼, 𝛾) & = ([𝛾 (⌜ 𝛼 (𝑥) ⌝)], 𝑑 (⌜ 𝛼 (𝑥) ⌝)) \\ = ([𝜓 (𝑑 (⌜ 𝛼 (𝑥) ⌝))], 𝑑 (⌜ 𝛼 (𝑥) ⌝)) \\ = 𝑔_{𝜓} ([𝛼 (⌜ 𝛼 (𝑥) ⌝)], 𝑑 (⌜ 𝛼 (𝑥) ⌝)) \\ = 𝑔_{𝜓} (𝑓 (𝛼, 𝛼)) \end{aligned}

这个等式成立的原因是 $𝑔_{𝜓}$ 本身不改变第二个分量， $𝑓$ 产生的第二个分量不依赖第二个参数，然后我们手动构造 $𝛾$ 让其产生一个 $𝜓 (𝑑 (-))$ 对应 $𝑔_{𝜓}$ 的输出形状。

因此 $𝑓 (𝛾, 𝛾)$ 是 $𝑔_{𝜓}$ 的不动点。注意第一个分量： $[𝛾 (⌜ 𝛾 (𝑥) ⌝)] = [𝜓 (⌜ 𝛾 (⌜ 𝛾 (𝑥) ⌝) ⌝)]$ ，即 $𝜑 = 𝛾 (⌜ 𝛾 (𝑥) ⌝)$ ，并且 $𝑸 ⊢ 𝜑 \leftrightarrow 𝜓 (⌜ 𝜑 ⌝)$

Remarks

以下 Remark 的理论 T 以 Q 或者 PA 为例，结构是指这个理论的结构。

Gödel’s first incompleteness theorem (original): 定义二元谓词 $Prov (𝑦, 𝑥)$ 为 “y 是某一语句的证明的编码，这一语句的编码是 x”。令 $𝜓 (𝑥) ≝ \forall 𝑦 (\neg Prov (𝑦, 𝑥))$ 。不动点 $𝜑 \leftrightarrow \forall 𝑦 (\neg Prov (𝑦, ⌜ 𝜑 ⌝))$ 等价于自身的不可证性。

Consistency 给出 $𝑻 ⊬ 𝜑$ 。
如果 $𝑻 ⊢ \neg 𝜑$ ，也就是 $\exists 𝑦 (Prov (𝑦, ⌜ 𝜑 ⌝))$ ，在 Non- $𝜔$ -consistent 的理论中，这可能被一个非标自然数验证。对于 $𝜔$ -consistency 理论，同时有 $𝑻 ⊬ \neg 𝜑$ 。

Gödel-Rosser’s incompleteness theorem: 令 $Neg$ 表示 Gödel number 上添加一个逻辑取反的符号： $Neg (⌜ 𝛼 ⌝) ≝ ⌜ \neg 𝛼 ⌝$ 。令

𝜓 (𝑥) ≝ \forall 𝑦 (Prov (𝑦, 𝑥) \to \exists 𝑧 (𝑧 < 𝑦 \land Prov (𝑧, Neg (𝑥))))

即对于任意 $𝑥$ 的证明 $𝑦$ ，都存在一个比 $𝑦$ 更小的，not $𝑥$ 的证明。将其不动点称为 $𝜑$ 。

如果 $𝑇 ⊢ 𝜑$ ，那么存在一个 $𝑛 \in ℕ$ ， $𝑇 ⊢ Prov (𝑛, ⌜ 𝜑 ⌝)$ ，因此存在一个更小的逻辑取反的证明，只有有限个可能，可以在 PA / Q 内枚举验证，矛盾。
如果 $𝑇 ⊢ \neg 𝜑$ ，即 $𝑇 ⊢ \exists 𝑦 (Prov (𝑦, ⌜ 𝜑 ⌝) \land \forall 𝑧 (Prov (𝑧, Neg (⌜ 𝜑 ⌝)) \to 𝑧 \geq 𝑦))$ 。注意到存在一个 $𝑛 \in ℕ$ 验证了 $Prov (𝑛, Neg (⌜ 𝜑 ⌝))$ ，因此 $\exists 𝑦 \leq 𝑛 (Prov (𝑦, ⌜ 𝜑 ⌝))$ ，这只有有限个可能，可以在 PA / Q 内枚举验证，矛盾。

所以 Rosser’s trick 去掉了对于 $𝜔$ -consistency 的要求。

Gödel’s second incompleteness theorem: 找一个明显有矛盾的语句，例如在等值逻辑+Q 上，令 $⊥ ≝ 0 = 1$ 。一个理论是 Consistent 的 iff. 它不能证明 $⊥$ ，所以定义 $Con (𝑻) ≝ \neg \exists 𝑥 (Prov (𝑥, ⌜ ⊥ ⌝))$ 。令 $𝜑$ 表示我们在原先 First incompleteness theorem 中构造的在 T 中可证和自身不可证明性等价的语句。注意到我们可以把整个 First incompleteness theorem 的证明也在 T 内部编码，所以 $𝑻 ⊢ Con (𝑇) \to \neg \exists 𝑥 (Prov (𝑥, ⌜ 𝜑 ⌝))$ ，也就是 $𝑻 ⊢ Con (𝑇) \to 𝜑$ 。

因此，如果有 $𝑻 ⊢ Con (𝑇)$ ，那么 $𝑻 ⊢ 𝜑$ ，与 First incompleteness theorem 矛盾。

Tarski’s undefinability theorem: 如果存在一个可定义谓词 $𝑇 (𝑛)$ 描述 $⌞ 𝑛 ⌟$ 在某个特定结构 $𝑀$ 中的真实性，那么定义 $𝜓 (𝑛) ≝ \neg 𝑇 (𝑛)$ ，不动点 $𝜑 \leftrightarrow \neg 𝑇 (⌜ 𝜑 ⌝)$ 是 $𝑇$ 上述性质的反例。

References:

A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points (Yanofsky) (2003) 比较经典的 Text，使用集合的方法描述的对角线方法，但是对于 Diagonal lemma 的处理有些不良定义的地方。
Diagonalization as computation: Gödel sentence construction and a type-disciplined blueprint (Vestrucci) (2026) 上了 Type 之后修正之后的 Text

Caveats

事实上这里有很多很多坑：

如果尝试直接定义 $ℕ$ 子集范畴，态射是所有语言的 total computable 函数（都可以在 Q 里面定义），然后找一个 $𝐹$ 是所有语句的 Gödel 编码集合，看上去 $𝑓 : ℕ \to 𝐹^{ℕ}$ 直接就工作了。但是这里有个问题：这个 $𝑓$ 的值域是受限的，所以不能直接定义成 id，而是必须得有一个方法检查一个整数是不是一个 $ℕ \to 𝐹$ 的编码，也就是要判断任意函数的值域是不是一个语句的 Gödel 编码。In general，这应该是 Undecidable 的。

Gödel numbering does not factor through Lindenbaum classes，对于 $𝜓 \leftrightarrow 𝜑$ ，可能存在谓词 $𝛾$ 使得 $𝛾 (⌜ 𝜓 ⌝)$ 和 $𝛾 (⌜ 𝜑 ⌝)$ 真值不同，所以一定有 $𝑸 ⊬ 𝛾 (⌜ 𝜓 ⌝) \leftrightarrow 𝛾 (⌜ 𝜑 ⌝)$ 。这是 Yanofsky 的构造中的漏洞。

Remarks

很多 Diagonal lemma 的用途在于 Computability theory，所以一般范畴中的态射可以不只是可定义函数，而是变成可计算函数，然后额外引入一个假设是所有可计算函数在我们关心的语言内都可以定义。Q 和 PA 都满足这一点。

模型大小

一阶逻辑有 Löwenheim-Skolem. 事实上 LS 跟完备性非常相关。Notably，以下两种逻辑因为能够控制模型大小，所以丧失了完备性：

SOL 可以描述模型大小，原因是相比于一阶的理论，二阶理论的二阶量词 Quantify over 的是真的模型里的东西，而不只是 definable 的东西。经典例子： ${𝐏𝐀}^{𝟐}$ 没有非标模型，因为任何 ${𝐏𝐀}^{𝟐}$ 模型都有 $ℕ$ 前段，而 $ℕ$ 这个前段套进二阶归纳里面直接得到所有元素都在 $ℕ$ 里。
${Ind}^{2} ≔ \forall 𝑃 ((𝑃 (0) \land (\forall 𝑛, 𝑃 (𝑛) \to 𝑃 (𝑆 (𝑛)))) \to \forall 𝑛 𝑃 (𝑛))$
这直接导致了二阶逻辑甚至没有一个 sound and complete deduction system。True arithmetic $𝑇 (ℕ)$ 不 RE. 如果 ${𝐏𝐀}^{𝟐}$ 有完备的 deduction system，可以枚举 proof，那么就可以枚举在 ${𝐏𝐀}^{𝟐}$ 里面的语义后承。FOL sentences 是 SOL sentences 的一个 decidable fragment (纯语法性质)，所以这样 $𝑇 (ℕ)$ 也 RE 了。
$𝑇 (ℕ)$ 不 RE 的原因：考虑把 $𝑇 (ℕ)$ 作为公理集的理论。这个理论是一个完备的一阶理论 (syntactical completeness)，而且 consistent（它有个模型），根据 Gödel’s incompleteness theorem，它肯定不是 effectively axiomatizable，因此 $𝑇 (ℕ)$ 不 RE。
事实上 ${𝐏𝐀}^{𝟐}$ 可以说明 SOL 不 compact. 符号集加一个常元 $𝑐$ ，考虑
$Γ = {𝐏𝐀}^{𝟐} \cup {𝑐 \neq 𝑆^{𝑛} (0) | 𝑛 \in ℕ}$
如果只考虑 FOL 的有限模型 (finite model theory)， valid FOL sentences are not RE. 与之对比，在任意模型内，根据 Completeness theorem, 枚举 proof 就可以枚举 valid sentences 了。See: Trakhtenbrot’s theorem.
因此，在 FOL 的这种解读下，General FOL 也不存在 sound and complete deduction system。

类型体操

#type @ 2026-08-08T20:35:55+08:00

Eliminator

Rocq 和 Agda 的 Inductive type 的 Elimination 都是 pattern matching as intrinsic, induction principle 是生成出来的。因此有的时候为了写明白 motive 会比较麻烦。

Characterizing inductive / coinductive / recursive types

常见的 (Co)inductive type 刻画方式有三种：考虑一个长相是 constructors 的 function / functor $𝐹$

$𝐹$ 的最小 / 最大不动点：将所有类型简单解读到 Set-valued semantics 上时的刻画
$𝐹 -$ iteration 的 colimit / limit：这是 Domain theory 里面的刻画，最常见的例子是 Haskell
Initial $𝐹$ -algebra / Final $𝐹$ -coalgebra，这是 General categorical semantics 里面通过 Universal property 的刻画

每一个都可以看作前一个的泛化。

首先只讨论递归类型只有严格正出现的情况，也就是最传统意义上的 Inductive / coinductive types。

Set-valued semantics

一个最简单的语义构造方法是把类型解读为“所有可能值构成的集合”。e.g. 考虑一个装配了 Type functor + fixpoint operator 的 STLC，我们可以把所有值解读为 Lambda 项的树形结构，类型解读为这些树的集合。可以把这些集合通过包含关系组成一个偏序，这构成一个 $𝜔 -$ 带底完备偏序 ( $𝜔 -$ dCPO)。^[证明?]

上述 $𝐹$ 是 $𝜔 -$ Scott-continuous 的。 ^[证明?] Kleene’s Fixed-point Theorem 可以用于构造 $𝐹$ 的最小不动点：

𝜇 𝐹 ≝ sup_{𝑛 \in 𝜔} 𝐹^{𝑛} (\emptyset) = lim_{𝑛 \in 𝜔} 𝐹^{𝑛} (\emptyset)

如果我们有办法找到一个“全集” $𝑈$ （通常来说解读比较正常的话总会有的，毕竟所有计算最多可数，找个大基数然后 Filter 一下就行了），那么我们把 $𝑈$ 扔进模型的 Universe 里面，虽然这个 $𝑈$ 是无法 Internally 定义的，但是可以把它当作顶，^{[ $𝜔 -$ cocompleteness?]} 这允许我们干两件事：

用 Kleene’s Fixed-point Theorem 的对偶构造最大不动点， $𝐹$ 也是 $𝜔 -$ co-Scott-continuous 的 ^[证明?]：

𝜈 𝐹 ≝ inf_{𝑛 \in 𝜔} 𝐹^{𝑛} (𝑈) = lim_{𝑛 \in 𝜔} 𝐹^{𝑛} (𝑈)

如果我们补充任意 Universe 中集合的并（比如直接把 $𝑈$ 的所有子集加进去），这时 $𝜔$ -dCPO 会升级成一个完备格。Knaster-Tarski 定理可以以非构造的方式给出 $𝐹$ 的最小 / 最大不动点。这里只需要 $𝐹$ 单调。

\begin{matrix} 𝜇 𝐹 = ⋂ {𝑥 \subseteq 𝑈 | 𝐹 (𝑥) \subseteq 𝑥} \\ 𝜈 𝐹 = ⋃ {𝑥 \subseteq 𝑈 | 𝐹 (𝑥) \supseteq 𝑥} \end{matrix}

Domain theory

Set-valued semantics 存在的问题是，想要最大不动点就必须引入一个全集，这个在语言里没有一个很明确的意思。以及接下来会说明 Haskell 的通常 Denotational semantics 解读中可以证明 $𝜇 \equiv 𝜈$ ，但是在 Set-valued semantics 中不是很显然为什么这两个迭代过程会收敛到同一个点上。核心的问题是，Kleene’s Fixed-point Theorem 只工作在一个偏序上，而偏序的 Antisymmetry 是一个很强的条件（Somewhat too rigid）。

首先以 Haskell 为例。

Haskell 会将 每一个类型都解读为一个 $𝜔$ -dCPO，含义和 Set-valued semantics 完全不同，这里的序是不同的值/表示之间的序，而不是不同类型之间的序。值之间的序来自于 definedness: $𝑥 \leq 𝑦$ 被定义为 $𝑥$ less-defined than y。因为 Haskell 的 Non-strictness，每个类型都包含一个底 $⊥$ ，这样的偏序通常被称为 Domain。如果我们把所有类型收集起来，会构成一个范畴，称之为 $𝜔 - {CPO}_{⊥}$ 。这个范畴中的态射是 $𝜔 -$ Scott-continuous 函数。

注意！此时整个 $𝜔 - {CPO}_{⊥}$ 范畴上没有全局的对象间的序结构。在每个类型内，依旧还可以做 Kleene’s Fixed-point Theorem 迭代构造，但是此时只有底，所以只能构造出类型上自映射的最小不动点 (i.e. fix)，是一个值。自映射函数的最大不动点值是一个不良定义的概念。

在 $𝜔 - {CPO}_{⊥}$ 范畴上构造类型不动点的方式是通过 Adamek’s Theorem。 $𝜔 - {CPO}_{⊥}$ 存在 Initial / terminal object _{[严格来说这是错误的，在这个解读下这不是一个 Initial object: morphism 不唯一。不过我们可以在这里选 $⊥ \mapsto ⊥$ 的态射，这个迭代构造依旧成立]}，并且 $𝐹$ 保持 $𝜔 -$ limit / colimit。^[证明?]。Adamek’s Theorem 是 Kleene’s Fixed-point Theorem 的范畴化：

Adamek’s Theorem 只说明了这个构造能够得到 Initial $𝐹 -$ algebra / Final $𝐹 -$ coalgebra ^[证明?]，因此和最后一个通过 Universal property 的刻画联系起来了。具体为了让它们是不动点，需要：

Lambek’s Lemma: Initial $𝐹$ -algebra $(𝐴, 𝛼)$ 中的 Structure map $𝛼 : 𝐹 (𝐴) \to 𝐴$ 是一个同构。 Dually，Final $𝐹$ -coalgebra $(𝐵, 𝛽)$ 中的 $𝛽 : 𝐵 \to 𝐹 (𝐵)$ 也是一个同构。^[证明?]

注意到，这里有一点区别：Categorical semantics 中只要求这是一个同构，而不要求 $𝐹 (𝐴) = 𝐴$ 。如果我们把 Set-valued semantics 中的 $𝜔 -$ dCPO 视为一个范畴，偏序范畴中的同构就是相等，Adamek’s Theorem 的迭代构造正好是 Kleene’s Theorem。

事实上在 Haskell 里面 Mu 和 Nu 确实不是 Definitionally 相等的，它们的同构来自于 unfold + fold 是 bijective + invertible 的。

About negative occurrences

负出现会破坏上述通过 Kleene’s FP Theorem / Adamek’s Theorem 的构造方式：

Set-valued semantics 中， $𝐹$ 不再是 monotone 的，所以一定不 Scott-continuous, Kleene’s FP Theorem 不再适用。
范畴中， $𝐹$ 的 Variance 变化（变成 Contravariant 或者更糟地，Mixed variance 或者根本不是一个 Functor），所以上述 Diagram 不再是一个链。

解决这个问题的方式是给 $𝐹^{𝑛 ({⊥})}$ 迭代中的态射一些额外的结构/关系：Embedding-projection pair。在 $𝜔 - {CPO}_{⊥}$ 中，反复应用 $𝐹$ 可以视作将一个类型“细化”：原先的值原样包含，新的值来自于原先值中的 $⊥$ 被多 Define 一层。因此每迭代一次可以看作将之前的值嵌入到一个更大的类型中。Embedding-projection pair 包含两个态射：

𝐴 ⇄_{𝑝}^{𝑒} 𝐵

其中 $𝑝 \circ 𝑒 = id, 𝑒 \circ 𝑝 \leq id$ (ordering on morphisms is defined pointwise)

在 EP-pair 的帮助下，可以拧转负出现带来的 Variance 变化。e.g.:

data T = C1 | C2 T T | C3 (T -> ())

迭代 0 次： $𝟎 = ⊥$
迭代 1 次： $𝐹 (𝟎) = ⊥, C1, C2 ⊥ ⊥, C3 {⊥ \mapsto ()}, C3 {⊥ \mapsto ⊥}$
迭代 2 次：
$\begin{matrix} 𝐹^{2} (𝟎) = ⊥, C1, C2 ⊥ ⊥, C2__, \\ C3 {⊥ \mapsto (), C1 \mapsto (), C2 ⊥ ⊥ \mapsto (), C3 {⊥ \mapsto ()} \mapsto (), C3 {⊥ \mapsto ⊥} \mapsto ()}, \dots \end{matrix}$
…

第一次迭代的 Embedding-projection pair 可以直接被写出：

$𝑒_{0} = {⊥ \mapsto ⊥}$ （注意这里 $𝑒$ 不能随便选了）
$𝑝_{0} = {_\mapsto ⊥}$

接下来， $𝑒_{𝑛} = 𝐹 (𝑒_{𝑛 - 1}), 𝑝_{𝑛} = 𝐹 (𝑝_{𝑛 - 1})$ ，具体 Ctor 中每个分量作用在 EP-pair 上的行为取决于 Ctor 的 Variance：

C1 不作用： $𝑒_{𝑛} (C1) = C1, 𝑝_{𝑛} (C1) = C1$ 。
$𝑒_{𝑛} (C2 𝑥 𝑦) = 𝐹 (𝑒_{𝑛 - 1}) (C2 𝑥 𝑦) = C2 𝑒_{𝑛 - 1} (𝑥) 𝑒_{𝑛 - 1} (𝑦)$ , $𝑝_{𝑛} (C2 𝑥 𝑦) = 𝐹 (𝑝_{𝑛 - 1}) (C2 𝑥 𝑦) = C2 𝑝_{𝑛 - 1} (𝑥) 𝑝_{𝑛 - 1} (𝑦)$
注意到右复合 $𝑝_{𝑛 - 1}$ 可以将函数作用域提高一次迭代，右复合 $𝑒_{𝑛 - 1}$ 可以将函数作用域降低一次迭代，因此这里有一次拧转： $𝑒_{𝑛} (C3 𝑓) = C3 𝑓 \circ 𝑝_{𝑛 - 1}$ , $𝑝_{𝑛} (C3 𝑔) = C3 𝑔 \circ 𝑒_{𝑛 - 1}$

可以验证对于所有 $𝑛$ , $𝑒_{𝑛}$ 和 $𝑝_{𝑛}$ 都构成一组 EP-pair. 这样修过以后的 Functor $𝐹$ 一定是 Covariant 的。在这个基础上可以直接用 Adamek’s Theorem。注意到， $𝐹$ 不是在原来的 $𝜔 - {CPO}_{⊥}$ 范畴上定义的，而是其一个只包含 EP-pair 的子范畴。假设最终得到的 (Co)limit 是 $𝐹_{𝜔}$ ，根据 Lambek’s Lemma, $𝐹_{𝜔} ≃ 𝐹 (𝐹_{𝜔})$ 。又因为 $𝐹_{𝜔} ⇆_{𝑝_{𝜔}}^{𝑒_{𝜔}} 𝐹 (𝐹_{𝜔})$ ，所以 $𝑒_{𝜔}$ 和 $𝑝_{𝜔}$ 就是这个同构。它们的名字叫 unfold 和 fold。

Bonus: ${⊥}$ 同时是 Embedding subcategory 的 Initial object 和 Projection subcategory 的 Terminal object。可以在这两个子范畴中分别做 Adamek’s Theorem，因此 Haskell 中 Mu A 和 Nu A 永远同构。

About uniqueness

上述内容中有部分过度简化：

在 $𝜔 - {CPO}_{⊥}$ 中， ${⊥}$ 并不是 Initial object，因为一个 Non-strict 态射可以将 $⊥$ 映射到任何值上。事实上，Mu A 甚至通常不是 Initial $𝐹 -$ algebra，对于任意的 Endofunctor $𝐹$ ，在 $𝜔 - {CPO}_{⊥}$ 中 Initial $𝐹 -$ algebra 也无法保证存在。通常来说，我们要求 Initiality 只能是在 $𝜔 - {CPO}_{⊥}$ 的 strict subcategory 内，也就是只包含 Strict morphisms 的子范畴。

一个范畴中对于 Endofunctor $𝐹$ 如果 Initial $𝐹 -$ algebra 和 Final $𝐹 -$ coalgebra 永远存在且永远一致，那么这个范畴被称为 Algebraically compact，See: https://ncatlab.org/nlab/show/algebraically+compact+category 。如果 $𝐹$ locally continuous + covariant，那么 $𝐹 -$ algebra 和 $𝐹 -$ coalgebra 在 Strict subcategory 内是良定义的。Mu F 和 Nu F 同构，并且在 Strict subcategory 内分别是 Initial $𝐹 -$ algebra 和 Final $𝐹 -$ coalgebra，因此 Strict subcategory 对于这一类 Endofunctor 是 Algebraically compact 的。对于 Mixed variance，需要使用 Bifree algebra 定义。

About strictness

上述范畴内的构造可以被推广到 Strict language 内，例如 OCaml。此时类型可以没有底（普通 ( $𝜔 -$ )-cpo，称为 predomain），可以通过手动引入一个 Thunk 来编码 Non-strictness:

type strict_nat = O | S of strict_nat
type lazy_nat = LO | LS of (unit -> lazy_nat)

此时，Initial object 变成了 $\emptyset$ ，Terminal object 是 ${1}$ 。

在类型中添加一个底 $⊥$ 的操作称为 Lifting monad，Thunking 可以认为直接对应 Lift。

在 Predomain 中同样可以通过 EP-pair 构造任意 Recursive type。区别是因为 Initial / terminal object 不同，Category of predomains 不一定是 Algebraically compact 的。

See:

Call-by-push-value: https://pblevy.github.io/papers/hosc05.pdf 在 CBPV 中，明确拆分了 Thunking 和 Lifting 操作，成为了一对 Adjoint functor，因为它明确拆分了 Value category 和 Computation category。在传统的 Domain theory 中，Thunking 和 Lifting 是混在一起的，成为了一个 monad。
Lecture Note on Monad-Based Programming @ FAU: https://www8.cs.fau.de/ext/teaching/sose2023/mbprog/mbprog-skript.pdf

Additional resources

Cornell CS 6110 Lecture Notes on Scott’s $𝐷_{\infty}$ Construction: https://www.cs.cornell.edu/courses/cs6110/2014sp/Lectures/lec24.pdf
Domain Theory: Corrected and expanded version (Abramsky, Jung) (1994): https://www.cs.ox.ac.uk/people/stephen.abram/DomainTheory.pdf 对经典 Domain theory 经典且全面的综述
The Category-Theoretic Solution of Recursive Domain Equations (Smyth, Plotkin) (1982): 系统化了通过 Order-enriched categories, EP-pair 求解 Recursive type 的方法
Algebraically complete categories (Freyd) (1991): 比较现代的 axiomatic domain theory 的奠基性论文，通过 Dialgebra / Bifree algebra 解决 Mixed variance，并通过此定义 Algebraically compact category

愿望单

#wishlist @ 2026-04-01T12:50:05+08:00

学一下 NTT 和 FFT，看看怎么用在 Reed-Solomon decoder 上的。
把 dependent destruction 引入 JMeq 的细节搞明白。
Basic Schnorr signature, EdDSA, 为什么 EdDSA 比 ECC 在常见硬件上更快。有专有指令/加速器的可能吗？
NoC deadlock freedom

初等代数

#alg @ 2026-03-23T03:08:38+08:00

代数课没有好好听，注定度过失败的一生了。

Montgomery 模乘

在真实计算机中，不同带余除法的代价不同：比如除以 power of 2 非常便宜。Naive 的模乘实现需要用模数作为被除数，代价不好控制。Montgomery 模乘可以将计算过程中的除法替换为另一个被除数。

$𝑎, 𝑏 \in ℤ_{𝑞}$ ，需要计算 $𝑎 \cdot 𝑏 \in ℤ_{𝑞}$ ，如果 $ℤ_{𝑞}$ 中的元素都使用最小非负代表元表示，这就是要计算 $(𝑎 \cdot 𝑏) mod 𝑞$ 。假设有另一个常数 $𝑅 \in ℕ$ 满足 $𝑅 > 𝑞$ 而且两者互素。假设除以 $𝑅$ 的代价较小。

称 $𝑥 \in ℤ_{𝑞}$ 的 Montgomery 形式 $\tilde{𝑥} = 𝑥 \cdot 𝑅 \in ℤ_{𝑞}$ 。因为 $𝑅$ 的带余除法代价小，计算 $mod 𝑅$ 的代价很小。需要注意的是 $\cdot$ 和 $mod 𝑞$ 的代价较大。只要能够避免这两个操作，就能得到更快的模乘实现。

$𝑅^{*}$ 是 $𝑅$ 在 $ℤ_{𝑞}$ 里面的逆元， $𝑞^{*}$ 是 $𝑞$ 在 $ℤ_{𝑅}$ 里面的逆元。

\begin{aligned} \tilde{𝑎 \cdot 𝑏} & = \tilde{𝑎} \tilde{𝑏} 𝑅^{*} mod 𝑞 \\ = (\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) 𝑅^{*} mod 𝑞 \end{aligned}

注意到 $\forall 𝑥 \in ℤ$ ：

(𝑥 - (𝑥 𝑞^{*} mod 𝑅) 𝑞) mod 𝑅 = (𝑥 - (𝑥 𝑞^{*} 𝑞)) mod 𝑅 = 0

所以 $(\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞)$ 一定是 $𝑅$ 的倍数，在 $ℤ$ 中计算 $(-) \cdot 𝑅^{*} mod 𝑞$ 相当于计算 $\frac{-}{𝑅} mod 𝑞$ ：

\begin{aligned} \tilde{𝑎 \cdot 𝑏} & = \tilde{𝑎} \tilde{𝑏} 𝑅^{*} mod 𝑞 \\ = (\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) 𝑅^{*} mod 𝑞 \\ = \frac{\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞}{𝑅} mod 𝑞 \end{aligned}

最后我们可以通过 Bound $(\tilde{𝑎} \tilde{𝑏} - (\tilde{𝑎} \tilde{𝑏} 𝑞^{*} mod 𝑅) 𝑞) / 𝑅$ 来消除最外面的 $mod 𝑞$ ：注意到因为 $𝑅 > 𝑞$ ，这个值一定在 $(- 𝑞, 𝑞)$ 之间。所以我们只需要比较这个值是否是负数，如果是就加上 $𝑞$ 就好了。

实现中的一些细节：

一般来说参数选择是 $𝑅$ 是比 $𝑞$ 大的最小支持高效计算的机器字。比如对于 Dilithium prime $𝑞 = 8380417 < 2^{23}$ ，可以选择 $𝑅 = 2^{32}$ 。
所有除了除以 $𝑅$ 以外的计算都可以在 $ℤ_{𝑅^{2}}$ 内进行。如果 $𝑅 = 2^{32}$ ，只需要有高效的 64 位加、减、乘法。
真实实现中一般不用 $𝑞^{*}$ ，而是用 $- 𝑞$ 在 $ℤ_{𝑅}$ 内的逆元，因为 $ℤ_{2} 𝑅$ 中的加法一般比减法好处理。如果本身就有高效的 $ℤ_{2} 𝑅$ 减法，同时比较正负比比较常数要快，那么应该是用 $𝑞^{*}$ 。

Gemini 给出的伪代码：

#include <stdint.h>

// 4236238847 is -q^(-1) mod 2^32
#define QINV_NEG 4236238847u 
#define Q 8380417u

uint32_t montgomery_mul(uint32_t a_mont, uint32_t b_mont) {
  uint64_t prod = (uint64_t)a_mont * b_mont;
  
  // Calculate the multiple of Q needed to clear the lower 32 bits
  uint32_t t = (uint32_t)prod * QINV_NEG;
  
  // Add the multiple of Q and shift out the lower 32 bits (which are now guaranteed to be 0)
  uint64_t u = prod + (uint64_t)t * Q;
  uint32_t res = u >> 32;
  
  if (res >= Q) {
      res -= Q;
  }
  
  return res;
}

通讯

#communication @ 2026-03-08T16:29:47+08:00

Rectangle property

在 MPC 设定下，如果暂时不考虑 Active malicious adversary 的话，节点的私有状态 $(𝑥_{𝑖}, 𝑟_{𝑖})$ i.e. 输入和随机性可以确定性决定 Transcript $𝑇$ 。将这一映射称为 $Π$ .

$Π^{- 1}$ 具有 “Rectangle property”， $\forall 𝑇 \in 𝒯︀, Π^{- 1} (𝑇)$ 是一个 Rectangle：

Π^{- 1} (𝑇) = \prod_{𝑖 = 1}^{𝑛} 𝜋_{𝑖} (Π^{- 1} (𝑇))

可以理解成，如果有任意两个所有 Party 的私有状态集合 $𝑆_{1}, 𝑆_{2}$ 满足 $Π (𝑆_{1}) = Π (𝑆_{2}) = 𝑇$ ，那么可以把 $𝑆_{1}$ 和 $𝑆_{2}$ 任意组合（每个 Party 任意在两者中选一个），那么最终 Transcript 依旧是 $𝑇$ 。

证明把 T 当成一个消息列，归纳。

这有两个很直接的后果：

如果至少有 3 个 Party，那么不存在在纯广播信道上的 $𝑡 \geq 1$ 的计算元素和的协议。原因是如果存在，假设 Party 1 semi-honest，Fix $(𝑥_{1}, 𝑟_{1})$ ，注意到只要 $\sum_{{𝑖 \geq 2}} 𝑥_{𝑖}$ 不变，那么 Party 1 的 View 也不变。这是纯广播，因此 Transcript 不变。只要有限域大小大于 2, 总能选出来两个不同的元素 $𝑒_{0}, 𝑒_{1}$ ，假设他们是 Party 2 和 Party 3 的输入，那么交换他们，Party 1 View 不变，所以把 Party 3 的输入从 $𝑒_{1}$ 改成 $𝑒_{0}$ ，Party 1 View 依旧不变，但是结果变了，矛盾。
不存在 2-Party 计算 AND 的协议。如果存在， $𝑥_{1} = 0, 𝑥_{2} = 1$ 和 $𝑥_{1} = 1, 𝑥_{2} = 0$ 都会输出 $0$ , 所以 Adversary View 相同，只有两个 Party 所以 View 包含整个 Transcript，整个 Transcript 也就相同。所以 $𝑥_{1} = 𝑥_{2} = 1$ 也应该产生一样的 Transcript，但是这会产生不同的输出，矛盾。

相关历史综述见 Gemini DeepResearch。AI 幻觉有风险，4.6 Opus 就给我幻觉了几个 Ref。不过 DeepResearch 至少给链接了。

Reed-Solomon 纠错

Reed-Solomon 如果有 $2 𝑡$ 冗余可以纠 $𝑡$ 个错 (Also, Shamir Secret Sharing).

考虑有限域 $GF (𝑞)$ 上的 Reed-Solomon 码，共 $𝑛 - 2 𝑡$ 个数据， $2 𝑡$ 个冗余，总共采样点 $𝑛$ 个。现在要找出来其中最多 $𝑡$ 个错的点。如果我们忽略多项式的其他结构，认为这些采样点是任选的，下面陈述的方法是找到这些错误点的标准方法 Berlekamp-Welch algorithm。

Berlekamp-Welch

假设 Underlying polynomial 是 $𝐹 (𝑥)$ ，Claim 存在一个多项式 $𝐸 (𝑥)$ ，满足 $𝑥_{𝑖} incorrect \Leftrightarrow 𝐹 (𝑥_{𝑖}) \neq 𝑦_{𝑖} \Rightarrow 𝐸 (𝑥_{𝑖}) = 0$ 。如果 $𝑥_{𝑖}$ 不是错误的点，对 $𝐸 (𝑥_{𝑖})$ 没有要求。因为最多 $𝑡$ 个错误，所以我们可以要求 $deg 𝐸 (𝑥) = 𝑡$ ，并且最高次项系数为 $1$ ， $𝐸 (𝑥)$ 剩下 $𝑡$ 个系数未知。

$𝐸 (𝑥_{𝑖}) 𝐹 (𝑥_{𝑖}) = 𝐸 (𝑥_{𝑖}) 𝑦_{𝑖}$ 对所有采样点成立。这给我们提供了 $𝑛$ 个方程， $deg 𝐹 (𝑥) = 𝑛 - 2 𝑡 - 1$ ，令 $𝑄 (𝑥) = 𝐸 (𝑥) 𝐹 (𝑥)$ ， $deg 𝑄 (𝑥) = 𝑛 - 𝑡 - 1$ ，线性系统 $𝑄 (𝑥_{𝑖}) - 𝐸 (𝑥_{𝑖}) 𝑦_{𝑖}$ 一共 $𝑛$ 个方程， $𝑛$ 个未知数，可以解出 $𝑄 (𝑥)$ 和 $𝐸 (𝑥)$ ，之后 $𝐹 (𝑥) = \frac{𝑄 (𝑥)}{𝐸 (𝑥)}$ 或者 Chien search. 复杂度 $𝒪︀ (𝑛^{3})$

Alternatively, 这是一个 Rational polynomial interpolation 问题， $\frac{𝑄 (𝑥_{𝑖})}{𝐸 (𝑥_{𝑖})}$ 经过 $𝑛$ 个点。wo/ FFT 复杂度 $𝒪︀ (𝑛^{2})$ , w/ FFT 复杂度 $𝒪︀ (𝑛 {log}^{2} 𝑛)$ 。（但我都不会）

Generator view vs. evaluation view

有两种 (somewhat equivalent) 看待 Reed-Solomon code 的方式。

SSS 里常见的构造对应 RS code 的 Evaluation view，这也是 Reed & Solomon’s original view: 数据在 pre-defined points of evaluation. RS code 目前实现中常见的方法是 Generator view (BCH view): 数据在 polynomial coefficients 上。两者之间的转换就是一次 NTT.

令 $𝑚$ 为消息长度， $2 𝑡$ 为冗余， $𝑛 = 𝑚 + 2 𝑡$ 为 Codeword 长度。

对于 Generator view 的 RS code，预先选定的是一个 Generator polynomial $𝐺 (𝑥)$ ， $deg 𝐺 (𝑥) = 2 𝑡$ 。Underlying field $𝔽$ 满足 $| 𝔽 | = 𝑛 + 1$ ，要求 $𝐺 (𝑥) ∣ 𝑥^{𝑛} - 1$ 。

Generator polynomial 的常见构造方式是选定一个 $𝔽$ 的 primitive element $𝛼$ 和任意 $𝑟 \in ℕ$ , $𝐺 (𝑥) = \prod_{𝑖 = 1}^{2 𝑡} (𝑥 - 𝛼^{𝑖 + 𝑟})$ 。

对于 $𝑚$ 个消息 $𝑟_{0}, \dots, 𝑟_{𝑚 - 1}$ ，Message polynomial 是 $𝑀 (𝑥) = \sum_{𝑖 = 0}^{𝑚 - 1} 𝑟_{𝑖} 𝑥^{𝑖}$ 。有两种编码方式得到 Codeword $𝐶 (𝑥)$ ：

简单编码直接让 $𝐶 (𝑥) = 𝐺 (𝑥) \cdot 𝑀 (𝑥)$ 。解码的时候需要做一次多项式除法
Systematic encoding 令 $𝐶^{'} (𝑥) = 𝑀 (𝑥) \cdot 𝑥^{2} 𝑡$ ，然后 $𝐶 (𝑥) = 𝐶^{'} (𝑥) - (𝐶^{'} (𝑥) mod 𝐺 (𝑥))$ 。Systematic encoding 的好处是前 $𝑚$ 个符号就是消息，解码的时候非常简单

Sidenote: 因为消息总能做 Padding，尤其是 Systematic encoding 里面消息 Padding 直接对应 Codeword padding，所以都可以不传这部分 Codeword。因此 $𝑛 = | 𝔽 | - 1$ 的限制事实上限制的是最大 Block length。Evaluation view 也有类似的限制，这个限制来自于 Evaluation point 的个数。但是因为可以选任意 $𝔽$ 元素当作 evaluation point，所以限制比 Generator view 要大 1. (Related: Extended RS & Doubly-extended RS，但是我没看懂这些)

Generator view decoding

在 Generator view 构造中，Berlekamp-Welch 无法直接使用。Berlekamp-Massey 是一个求最小 LFSR 的算法，在 RS code 中可以用于在 generator view 的构造中替代 Berlekamp-Welch 做错误定位。

注意到，两种 encoding 如果理解成 $𝑀 (𝑥) \mapsto 𝐶 (𝑥)$ 在 ${𝔽 [𝑥]}_{\leq 𝑚 + 2 𝑡 - 1}$ 多项式空间里的函数，都是可逆线性的。因为 $𝑀 (𝑥)$ 是一个 degree-m 子空间，因此所有无错误 Codeword 也是一个 degree-m 子空间。错误校验是判定一个多项式是否在这个空间内。

在这个多项式空间上取以下内积结构：系数乘积的和 (i.e. 选取 ${𝑥^{𝑖}}$ 做基映射到 $𝔽^{𝑛}$ )。 $𝐶 (𝑥)$ 。Codeword 空间的正交补空间 degree 是 $𝑚 + 2 𝑡 - 𝑚 = 2 𝑡$ ，因此可以通过 $2 𝑡$ 个多项式来 span 这个正交补空间。

定义 Parity-check polynomial $𝐻 (𝑥) = \frac{𝑥^{𝑛} - 1}{𝐺 (𝑥)}$ 。 $deg 𝐻 (𝑥) = 𝑛 - 2 𝑡 = 𝑚$ ，令 $𝐻^{*} (𝑥) = 𝑥^{deg 𝐻 (𝑥)} 𝐻 (𝑥^{- 1})$ 是 $𝐻 (𝑥)$ 的 Reciprocal polynomial。 ${𝐻^{*} (𝑥) \cdot 𝑥^{0}, 𝐻^{*} (𝑥) \cdot 𝑥, \dots, 𝐻^{*} (𝑥) \cdot 𝑥^{2 𝑡 - 1}}$ 是正交补空间的一组基。

他们是正交补空间的基的简短证明：这组基显然线性无关。同样， ${𝐺 (𝑥) \cdot 𝑥^{0}, 𝐺 (𝑥) \cdot 𝑥, \dots, 𝐺 (𝑥) \cdot 𝑥^{𝑚 - 1}}$ 是 Codeword 空间的一组基。为了证明他们是正交补，只需要证明两组基中任选向量内积为 0 即可。
注意到， $⟨ 𝐺 (𝑥) \cdot 𝑥^{𝑖}, 𝐻^{*} (𝑥) \cdot 𝑥^{𝑗} ⟩$ 正是表达式 $𝐺 (𝑥) \cdot 𝐻 (𝑥) mod (𝑥^{𝑛} - 1)$ 的 $deg 𝐻 (𝑥) + 𝑗 - 𝑖$ 次项系数。而 $𝐺 (𝑥) \cdot 𝐻 (𝑥) = 𝑥^{𝑛} - 1$

对于使用 Powers of primitive root 构造的 $𝐺 (𝑥)$ ，有更简单的办法给一组基。注意到任何 $𝐺 (𝑥)$ 的根 $𝛼^{𝑖}$ 都是 $𝐶 (𝑥)$ 的根，所以令 $𝐻_{𝑖} (𝑥) = \sum_{𝑗 = 0}^{2 𝑡} 𝑎^{𝑖 𝑗} 𝑥^{𝑗}$ ，那么 $⟨ 𝐻_{𝑖} (𝑥), 𝐶 (𝑥) ⟩ = 𝐶 (𝛼^{𝑖}) = 0$ ，因此 ${𝐻_{𝑖} (𝑥)}_{{𝑖 = 𝑟 + 1 \dots 𝑟 + 2 𝑡}}$ 是一组正交补空间的基。

上述构造出的正交补空间的基不一定正交，但是我们还是可以把 $𝐶 (𝑥)$ 投影上去，如果正确的编码是 $𝐶_{0} (𝑥)$ ，投影得到的结果是 $𝐸 (𝑥) = 𝐶 (𝑥) - 𝐶_{0} (𝑥)$ 也就是错误项在选定基下的坐标。这一坐标通常被称为 Syndrome ${𝑆_{𝑖}}_{𝑖 = 1 \dots 2 𝑡}$ 。

在使用 Power of primitive root 构造的 $𝐺 (𝑥)$ 的情况下，投影直接就是求值，因此不用存储 $𝐻$ 矩阵。

对于一般的 Parity-check matrix 构造，使用 Syndrome 进行错误定位可以利用 Meggitt Decoder: 一个查找表，加上 RS code 在 generator view construction 下是一个 Cyclic code 的特性检查。

Berlekamp-Massey

如果我们使用 Powers of primitive root 构造 $𝐺 (𝑥)$ 和 parity-check matrix $𝐻$ (as a Vandermond matrix of $𝛼, 𝛼^{2} \dots 𝛼^{2 𝑡}$ )，有更高效的做法。

假设 $𝐸 (𝑥)$ 里面实际有 $𝜈 \leq 𝑡$ 个错误 ${𝑒_{𝑗}}_{𝑗 = 1 \dots 𝜈}$ ，位置分别在 $𝑖_{1}, \dots, 𝑖_{𝜈}$ 次项，也就是：

𝐸 (𝑥) = \sum_{𝑗 = 1}^{𝜈} 𝑒_{𝑖_{𝑗}} 𝑥^{𝑖_{𝑗}}

因此 $𝑆_{𝑖} = 𝐸 (𝛼^{𝑖})$ 。现在的目标是找到 ${𝑖_{𝑗}}_{𝑗 = 1 \dots 𝜈}$ 。定义 Error locator polynomial:

Λ (𝑥) = \prod_{𝑗 = 1}^{𝜈} (1 - 𝑥 𝛼^{𝑖_{𝑗}})

$Λ (𝑥)$ 的根为 ${𝛼^{- 𝑖_{𝑗}}}_{{𝑗 = 1 \dots 𝜈}}$ 。假设 $Λ (𝑥)$ 展开为 $1 + Λ_{1} 𝑥 + Λ_{2} 𝑥^{2} + \dots + Λ_{𝜈} 𝑥^{𝜈}$ ，可以证明对于任意给定的正整数 $𝑗 \leq 2 𝑡 - 𝜈$ (见 Wikipedia)：

𝑆_{𝑗 + 𝜈} + Λ_{1} 𝑆_{𝑗 + 𝜈 - 1} + Λ_{2} 𝑆_{𝑗 + 𝜈 - 2} + \dots + Λ_{𝜈} 𝑆_{𝑗} = 0

注意到这等价于一个需要找到一个最短的 $𝜈$ -stage LFSR 生成 $𝑆_{1}, 𝑆_{2}, \dots, 𝑆_{2 𝑡}$ 。注意：对于一个 Recurrent sequence，如果我们知道他的 Generating LFSR has degree $\leq 𝑡$ ，那么可以通过前 $2 𝑡$ 项确定 Generating LFSR。但是反过来不成立： 存在 $2 𝑡$ 个元素序列无法被一个 degree $\leq 𝑡$ 的 LFSR 生成。

BM 算法的直觉是一个一个试，看看目前猜的 LFSR 有没有出错。保存一个上一次出错的时候的 LFSR，以及当时出的错 $𝑏$ ，如果这次出错 $𝑑$ ，那么把上次的 LFSR $\times \frac{𝑑}{𝑏}$ 减掉就可以用来修这次的错。Pseudocode in Rust format:

// Input: S: Vec<Field> of length 2t
let mut lambda = poly!(1); // C in most texts about BM
let mut last_lambda = poly!(1); // B in most texts about BM
let mut last_update = -1;
let mut last_dis_inv = 1;

for k in 0..2t {
  // Loop invariant:
  // last_lambda when evaluates by S[..last_update
  // will generate discrepancy last_dis_inv^(-1)
  let discrepancy = S.rev().skip(2 * t - k - 1) // Start from S[k]
    .zip(lambda.coeffs()) // Coeffs from lowest degree to highest
    .map(|(s, l)| s * l)  // Field multiplication
    .sum();               // Field addition
  if discrepancy == 0 { continue; }
  let tmp = lambda.clone();
  let update = (discrepancy * last_dis_inv)
    * last_lambda * poly!(x^(k - last_update));
  // Because of the invariant, the update polynomial
  // will evaluates to exactly discrepancy at S[..k]
  lambda -= update;

  if lambda.degree() > tmp.degree() {
    // Degree updated
    last_lambda = tmp;
    last_update = k;
    last_dis_inv = 1 / discrepancy;
  }
}

lambda / lambda.coeffs().first()
// So that the constant term is always 1

Loop invariant -> 算法正确性。找到的 LFSR 肯定是一个成立的。最小性原因是我们在 Degree 上升的时候更新用来修 Discrepancy 的多项式，证明待补充（我还没看懂，乐）

Other notes

现代解读中会把 BM 当成 Padé approximation 的一个特例，在这个解读下它的对面是扩展欧几里得。现代 RS decoder 也有很多通过 EEA 实现的。可能需要继续阅读以下内容：

Forney algorithm: 在已知错误位置后计算错误值。在其中定义的 Error evaluator 是将 RS decoding 建模为 Padé approximation 问题的基础。
Modified Euclidean Algorithms for Decoding Reed-Solomon Codes

Hello, World!

#hello-world @ 2026-03-07T16:20:35+08:00

Hello! 这是 [喵喵](@CircuitCoder) 的笔记本。这里记录了我一些未经整理的笔记和想法，反映我的小脑瓜里在想什么，因此绝大多数内容会使用最接近我思考的中英混杂写成，请见谅。

制作这个笔记的动机是想有一个类似[杰哥](@jiegec)的知识库，但是考虑到我的知识一点都没有结构性，所以正好就做成了这样一个杂乱无章的 UI，非常合适。

这里的想法成熟之后可能会整理变成我的博客的帖子，内容也可能会随便删改修订，如果需要 Permalink 的话请复制每个 Section 标题下方更新日期的那个链接，那个链接带有 Commit Hash，可以保证不变。

这里没有评论区，可以直接在 Repo 的 Issue section 发 issue。

Git Repo: CircuitCoder/scribble

逻辑

Lawvere’s Fixed-point Theorem

Cantor’s proof of 𝒫︀(𝐴)>𝐴

Turing’s Halting problem

Caveats & further remarks

Gödel’s diagonal lemma

Remarks

Caveats

Remarks

模型大小

类型体操

Eliminator

Characterizing inductive / coinductive / recursive types

Set-valued semantics

Domain theory

About negative occurrences

About uniqueness

About strictness

Additional resources

愿望单

初等代数

Montgomery 模乘

通讯

Rectangle property

Reed-Solomon 纠错

Berlekamp-Welch

Generator view vs. evaluation view

Generator view decoding

Berlekamp-Massey

Other notes

Hello, World!

Cantor’s proof of $𝒫︀ (𝐴) > 𝐴$