Homological Invariants of Higher-Order Equational Theories

Many first-order equational theories, such as the theory of groups or boolean algebras, can be presented by a smaller set of axioms than the original one. Recent studies showed that a homological approach to equational theories gives us inequalities to obtain lower bounds on the number of axioms. In this paper, we extend this result to higher-order equational theories. More precisely, we consider simply typed lambda calculus with product and unit types and study sets of equations between lambda terms. Then, we define homology groups of the given equational theory and show that a lower bound on the number of equations can be computed from the homology groups.