论文标题
通过同源方法获得的重写规则数量的下限
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
论文作者
论文摘要
众所周知，某些方程理论（例如组或布尔代数）可以由比原始公理更少的方程公理来定义。但是，确定给定的公理是否最小并不容易。 Malbos和Mimram研究了一种使用同源代数的代数（或术语重写系统）等同于给定的方程理论（或术语重写系统）的一组方程公理（或重写规则）的基数的一般方法。他们的方法是关于Squier的同源性理论的类似物。在本文中，我们开发了更多的术语重写系统的同源性理论，并在等价范围更强大的概念下提供了更好的下限。作者还实施了一个程序来计算下限，并进行了64个完整的TRS。
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.
