Homological Invariants of Higher-Order Equational Theories
This provides a theoretical tool for understanding the minimal axiomatization of higher-order equational theories, but the result is incremental as it generalizes existing first-order techniques.
The paper extends homological methods from first-order to higher-order equational theories, specifically for simply typed lambda calculus with product and unit types, showing that homology groups provide lower bounds on the number of equations needed to axiomatize a theory.
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.