一句话：用同调方法改进项重写系统的重写规则数下界，并实现计算与实验。
判定一个等式理论或项重写系统能否用更少的公理/重写规则等价定义并不容易。Malbos 和 Mimram 曾用同调代数给出等价公理集或重写规则集基数的一般下界，其方法类比字符串重写系统的 Squier 同调理论。本文进一步发展项重写系统的同调理论，在比前人更强的等价概念下导出更优的规则数下界。作者还实现了计算该下界的程序，并在 64 个完全项重写系统上进行了实验。
It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier's homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds, and experimented with 64 complete TRSs.
@article{paperbot1649,
title = {A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods},
author = {Mirai Ikebuchi},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:36)2022}
}