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.

翻译：众所周知,某些等式理论,如组合或布尔列安代数,可以用比原正数少的方程轴来定义。然而,很难确定某一组的正数是否最小。 Malbos和Mimram调查了一种一般方法,以找到一套方程轴(或重写规则)之基点的较低界限,该基点相当于一种特定方程理论(或术语重写系统),使用同义代数。它们的方法类似于Squier在字符串重写系统中的同理理论。在本文中,我们开发了术语重写系统的同理理论,在比等值更强的概念下提供了更低的约束。作者还实施了一种程序,以64个完整的 TRS为实验。