| Summary: | 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.
|
|---|