近自由代数：从单词问题到量消
逻辑
2026-04-28 v1
摘要
项代数是计算机科学中的重要对象，因而受到广泛关注。其自然推广是通过对这些代数取模，除以有限个 ground term 方程所得，称为近自由代数。近自由代数的最早结果之一是其单词问题是多项式时间可判定的。在本文中，我们证明其他自然问题：寻找标准代表项；计算同义类的基数；检查所有同义类是否无限；检查代数是否有限；检查两个代数是否同构，均为多项式时间可判定的。关于项代数的著名结果是它们在 suitably 扩充语言中容许量消。在此模式下，我们也证明了近自由代数通过在标准测试谓词中扩展语言来实现量消。虽然这一结果已被现有结果所暗示，但我们认为本文的主要贡献在于提供了一种不同的方法，我们相信可以轻易地扩展到既有作品未覆盖的更大类中。最后，我们提供了一个应用，用于量消程序，构建在任意签名下都具有多项式时间单词问题的非初始代数的示例。
引用
@article{arxiv.2604.23967,
title = {Almost free algebras: from the word problem to elimination of quantifiers},
author = {Yifan Jia and Heer Tern Koh and Bakh Khoussainov},
journal= {arXiv preprint arXiv:2604.23967},
year = {2026}
}