发表机构
National Taiwan University; Rice University（国立台湾大学; 莱斯大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文回顾Büchi补集构造历史，论证可用较弱同余引理替代Ramsey定理，倡导将基于Ramsey的构造更名为基于同余的构造。
AI 中文摘要
J. Richard Büchi本人提出的第一个用于补全Büchi自动机的构造依赖于一个关于将任意无限词划分为连续有限词的基本引理，该引理通过引用Ramsey的一个专门定理得到了简洁证明。因此，类似性质的构造随后被标记为基于Ramsey的。然而，只需该引理的一个较弱形式即可，其中有限词来自有限数量的同余类，而非任意类，这些同余类构成所有有限词集合的一个划分。借助同余的更好性质，这个较弱的引理可以在不使用Ramsey定理的情况下证明。对此类补集构造的一种常见改进也需要同余的运作。本文回顾了历史，并尽可能使用更现代的术语审视相关概念和结果，以倡导将基于Ramsey的构造重新命名为基于同余的构造。
英文摘要
The very first construction by J. Richard Büchi himself for complementing a Büchi automaton relies on a fundamental lemma about the division of an arbitrary infinite word into consecutive finite words, which was cleanly proven by invoking a specialized theorem of Ramsey. For that reason, constructions of similar nature have subsequently been labeled as Ramsey-based. Nevertheless, it suffices to have a weaker form of the lemma where the finite words come from a finite number of congruence classes, rather than arbitrary classes, that form a partition of the set of all finite words. The weaker lemma, with support of nicer properties from a congruence, can be proven without Ramsey's theorem. A commonly adopted improvement on such complementation constructions also requires the working of a congruence. This paper recounts the history and reviews using more contemporary terminology wherever possible the relevant concepts and results, to advocate renaming of Ramsey-based constructions as congruence-based constructions.
