Slava 的幺半兽园

# Slava 的幺半园 来源：https://factorcode.org/slava/monoids.html 返回我的主页（https://factorcode.org/slava） ## 目录 - 引言（https://factorcode.org/slava/monoids.html#introduction） - 字问题（https://factorcode.org/slava/monoids.html#wordproblem） - 有限完备重写系统（https://factorcode.org/slava/monoids.html#fcrs） - 本研究的目标（https://factorcode.org/slava/monoids.html#goal） - 两个生成元，两条关系（https://factorcode.org/slava/monoids.html#tworel） - 数据集（https://factorcode.org/slava/monoids.html#tworeldata） - *⟨a, b \| aaa=a, abba=bb⟩*（https://factorcode.org/slava/monoids.html#aaaaabbabb） - *⟨a, b \| aba=aa, baa=aab⟩*（https://factorcode.org/slava/monoids.html#abaaabaaaab） - 两个生成元，一条关系（https://factorcode.org/slava/monoids.html#onerel） - 数据集（https://factorcode.org/slava/monoids.html#onereldata） - 相关研究（https://factorcode.org/slava/monoids.html#relatedwork） - 次要结果（https://factorcode.org/slava/monoids.html#minorresults） --- ## 引言 我对**无限表示幺半群**（https://en.wikipedia.org/wiki/Presentation_of_a_monoid）的兴趣源于 Swift 编译器使用 **Knuth–Bendix 完备化算法**（https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm）来实现**同类型约束**。Knuth–Bendix 有多种实现方式，但在 Swift 中，它被用来解决**有限表示幺半群的字问题**（https://en.wikipedia.org/wiki/Word_problem_(mathematics)）。在 Swift 编译器里，这些有限表示幺半群就是函数和类型声明的泛型签名，其中的“关系”对应声明所施加的泛型约束。如果你感兴趣，所有细节都记录在《Compiling Swift Generics》（https://download.swift.org/docs/assets/generics.pdf）的第 16–18 章。 ## 字问题 字问题问的是：在给定一组双向字符串重写规则（即“关系”）下，两个有限字母表上的词是否等价。举个例子，假设有如下两条关系： 1. 🍌🍎🍌 = 🍎🍎🍎 2. 🍌🍌🍌 = 🍌🍌 你能把 8 个苹果组成的串 “🍎🍎🍎🍎🍎🍎🍎🍎” 变成 10 个苹果的串 “🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎” 吗？这绝非显而易见，事实上最少需要 15 步。（你可以玩这个[小游戏](https://factorcode.org/slava/babaaabbbbb/)亲自发现解法。）这就是字问题的具体实例：我们有两个词 *a⁸* 和 *a¹⁰*，以及幺半群表示 *⟨a, b \| bab=aaa, bbb=bb⟩*，想判断这两个词在这些规则下是否等价。 尽管上述表示很短，字问题却已相当困难。经典结果是：**有限表示幺半群的字问题在一般情况下不可判定**（https://en.wikipedia.org/wiki/Undecidable_problem）。一篇论文《An associative calculus with an insoluble problem of equivalence》（https://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=tm&paperid=1317&option_lang=eng）给出了一个极短的不可判定例子（英译与评注见 [G. S. Tseytin 的七关系半群](https://arxiv.org/abs/2401.11757)）： > *⟨a, b, c, d, e \| ac=ca, ad=da, bc=cb, bd=db, eca=ce, edb=de, cca=ccae⟩* ## 有限完备重写系统 Knuth–Bendix 试图从定义幺半群的双向等价关系构造出**有限完备重写系统**（FCRS）。FCRS 是一组**有向**的归约规则，能把任意词在有限步内归约到**范式**，从而完全解决字问题：给定两个词，先分别归约到范式，再看是否相同。 Knuth–Bendix 有时会失败——失败模式是无限运行，不断加入新规则却永不收敛。至少，如果输入规则定义的幺半群字问题不可判定，Knuth–Bendix 必定失败。 那么，若字问题可判定，是否总能用 FCRS 解决？Craig C. Squier 在 1980 年代末给出了否定答案。论文《A finiteness condition for rewriting systems》（https://www.sciencedirect.com/science/article/pii/0304397594901759）研究了幺半群 *S₁*： > *S₁:= ⟨a, b, t, x, y \| ab=1, xa=atx, xt=tx, xb=bx, xy=1⟩* Squier 证明 *S₁* 不具备**有限推导型**（finite derivation type），而这是存在 FCRS 的必要条件。因此，**任何表示该幺半群的生成集与归约序**，Knuth–Bendix 都无法成功。尽管如此，*S₁* 的字问题却是可判定的。 更短的例子（三生成元三关系）见论文《On finite complete rewriting systems, finite derivation type, and automaticity for homogeneous monoids》（https://www.sciencedirect.com/science/article/pii/S0890540117300937）： > *⟨a, b, c \| ac=ca, bc=cb, cab=cbb⟩* 该幺半群字问题可判定（关系保长度，先比长度再穷举即可），但仍无法用 Knuth–Bendix 完备化。 ## 本研究的目标 上述例子促使我开展以下研究： > **目标：**在某种主观意义下，找出“最小”或“最短”的幺半群表示，其字问题**无法**用有限完备重写系统（实际即某种 Knuth–Bendix 变体）解决。 为寻找 FCRS，我采用《Morphocompletion for one-relation monoids》（https://link.springer.com/chapter/10.1007/3-540-51081-8_141）的变体：引入新生成元，然后同时尝试多种归约序完成： - 所有字母序的 **Shortlex**（https://en.wikipedia.org/wiki/Shortlex_order） - 所有字母序与所有不同次数赋值的 **递归路径序**（https://en.wikipedia.org/wiki/Path_ordering_(term_rewriting)） 除了解决字问题，FCRS 还能告诉你该幺半群是否有限：若有限，可枚举元素、构造**Cayley 表**（https://en.wikipedia.org/wiki/Cayley_table）与**Cayley 图**（https://en.wikipedia.org/wiki/Cayley_graph）。也可判定 FCRS 是否表示一个**群**（https://en.wikipedia.org/wiki/Group_(mathematics)），进而找出生成元的逆元。我的支线任务便是收集并分析这些短表示的数据，见下方数据集。 最后你可能问： > **为什么？**因为这个问题有趣。 --- ## 两个生成元，两条关系 ## 数据集 对任意两生成元、两关系且**两边总长 ≤ 11** 的幺半群，我都能找到 FCRS，仅余 24 个例外，列于下页： **探索：** - [两生成元两关系幺半群](https://factorcode.org/slava/2211/) 枚举中大量实例以平凡方式“坍塌”： - *⟨a, b \| aa=a, ab=1⟩*（[第 4 例](https://factorcode.org/slava/2211/4.html)）是 1 元平凡群的表示，但还有 2030 个同构副本。 - *⟨a, b \| aa=1, ab=1⟩*（[第 1 例](https://factorcode.org/slava/2211/1.html)）是 2 元群的表示，但还有 1990 个副本。 - *⟨a, b \| aa=a, aaa=b⟩*（[第 236 例](https://factorcode.org/slava/2211/236.html)）是另一个 2 元幺半群；仅有 46 个副本。 枚举也包含若干经典有限群的短表示： - *⟨a, b \| abba=b, baba=1⟩*（[第 1427 例](https://factorcode.org/slava/2211/1427.html)）是 6 元**对称群**（https://en.wikipedia.org/wiki/Symmetric_group）的表示。（唯一非交换 6 元群，但非群的幺半群更多，例如略滑稽的 *⟨a, b \| ab=a, bbbb=ba⟩*（[第 3134 例](https://factorcode.org/slava/2211/3134.html)）。） - *⟨a, b \| aba=b, aabb=1⟩*（[第 556 例](https://factorcode.org/slava/2211/556.html)）是 8 元**四元数群**（https://en.wikipedia.org/wiki/Quaternion_group）。你能指出 i, j, k, −1 对应哪些元素吗？（分配方式不止一种。） - *⟨a, b \| aaa=1, abba=b⟩*（[第 747 例](https://factorcode.org/slava/2211/747.html)）是 27 元有限幺半群，而同表示的群是 **SL(2, 3)**（https://groupprops.subwiki.org/wiki/Special_linear_group:SL(2,3))。（幺半群多出 *a* 的幂次。） ## *⟨a, b \| aaa=a, abba=bb⟩* 我目前的主要结果是：**⟨a, b \| aaa=a, abba=bb⟩** 是**唯一**一个总长 10 的两生成元两关系幺半群，**在任何字母表上都无法用 FCRS 表示**（即“非 FCRS”）。事实上，与 Squier 的 *S₁* 类似，它**不具备有限推导型**。 **阅读证明：** - [一个两关系幺半群不具备有限推导型](https://factorcode.org/slava/aaaaabbabb.pdf) 注意，文章基于早期总长 10 的枚举，当时该 Monoid 是 3 个“硬”实例之一。此后我已为另外两个找到 FCRS： - *⟨a, b \| bab=aaa, bbbb=1⟩*（[第 4107 例](https://factorcode.org/slava/2211/4107.html)） - *⟨a, b \| aaaa=1, abbba=b⟩*（[第 5719 例](https://factorcode.org/slava/2211/5719.html)） ## *⟨a, b \| aba=aa, baa=aab⟩* 我还证明了一个总长 11 的“硬”实例也非 FCRS。主要证明仅两页，（相对）非常初等，只用到了**正则语言泵引理**（https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages）。我很乐意它成为某本字符串重写或 Knuth–Bendix 教材的例题！ **阅读证明：** - [幺半群 ⟨a, b \| aba=aa, baa=aab⟩ 无有限完备表示](https://factorcode.org/slava/abaaabaaaab.pdf) 一个我还没答案的有趣问题：该幺半群是否也不具备有限推导型？ 解决[两关系枚举](https://factorcode.org/slava/2211/)中剩余总长 11 的“硬”实例仍是开放问题。（眼尖的读者会发现，引言里的“8 苹果”幺半群 *⟨a, b \| bab=aaa, bbb=bb⟩* 就在其中。我敢打赌它非 FCRS。）有任何进展请告诉我！ --- ## 两个生成元，一条关系 我也研究了一条定义关系的幺半群。 ## 数据集 对任意两生成元、一条关系且**两边总长 ≤ 10** 的幺半群，我都能找到 FCRS，仅余 5 个例外，列于下页。目前**未知**是否所有单关系幺半群都能用 FCRS 表示。如果答案是否定的，也许其中一个例外就是首个反例！ **探索：** - [两生成元单关系幺半群](https://factorcode.org/slava/2110/) 枚举里可见若干经典单关系幺半群： - *⟨a, b \| ab=1⟩*（[第 2 例](https://factorcode.org/slava/2110/2.html)）是**双循环幺半群**（https://en.wikipedia.org/wiki/Bicyclic_semigroup）。 - *⟨a, b \| aba=1⟩*（[第 5 例](https://factorcode.org/slava/2110/5.html)）是整数加群。（你能看出为何 *ba=ab*，以及 *a*, *b* 分别对应哪个整数吗？） - *⟨a, b \| bab=aba⟩*（[第 123 例](https://factorcode.org/slava/2110/123.html)）是**3 股辫群**（https://en.wikipedia.org/wiki/Braid_group）*B₃* 的正词子幺半群，见论文《A finite Thue system with decidable word problem and without equivalent finite canonical system》。它在字母表 {*a*, *b*} 上无 FCRS，但若添加一个辅助生成元（等价于 *ab*, *ba* 或 *aba*）则可得 FCRS。 - *⟨a, b \| abbaab=1⟩*（[第 72 例](https://factorcode.org/slava/2110/72.html)）与 Jantzen 幺半群反同构，见《Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group》。要得到 FCRS（它其实是群），不仅要扩充生成集，还需使用允许**长度增加**规则的递归路径序。 本枚举**无有限幺半群**，因为两生成元至少需要两条关系才能表示有限幺半群。 **圣安德鲁斯大学**（https://www.st-andrews.ac.uk/）**James D. Mitchell**（https://www.st-andrews.ac.uk/mathematics-statistics/people/jdm3/）团队在用多种技术（不限于 FCRS）研究单关系幺半群的字问题，枚举范围更大——所有 *⟨a, b \| u=v⟩* 满足 |*u*| ≤ 10 且 |*v*| ≤ 10，而不仅仅是 |*u*| + |*v*| ≤ 10。参见他们的论文： - *Off with the head: termination provers and the word problem for 1-relation monoids*（https://www.imn.htwk-leipzig.de/WST2025/proceedings/WST2025_paper_16.pdf） - *Certifying the decidability of the word problem in monoids at large*（https://dl.acm.org/doi/10.1145/3779031.3779101） ## 次要结果 我解决了一些别人头疼的单关系幺半群字问题，或许有点意思！你会看到下面这种略滑稽的现象：从**一条**关系出发，最终却可能得到**大量**规则的有限完备重写系统。 **（1）**Victor Maltcev 给出的例子，见于 George M. Bergman《An invitation to General Algebra and Universal Constructions》（https://math.berkeley.edu/~gbergman/245/3.2.pdf）习题 4.10:8(ii)： > (ii) (Victor Maltcev) 对于由生成元 a, b 和关系 abbab = baabb 定义的幺半群，是否存在范式或其他有用描述？（我不知道答案。） 幺半群 *⟨a, b \| abbab=baabb⟩* 与 *⟨a, b \| abaab=aabba⟩*（[第 2675 例](https://factorcode.org/slava/2110/2675.html)）反同构，后者存在有限完备重写系统。 **（2）**下一个例子出自 C.F. Brodda 的精彩综述《The Word Problem for One-Relation Monoids》（https://arxiv.org/abs/2105.02853）： > 我们顺便指出，文献中尚无结果能解决的最小单项单关系幺半群是 ⟨a, b \| bababbbabba=a⟩。作者 n