一句话：将同调方法推广到高阶等式理论，用同调群计算等式公理数量的下界。
该论文研究高阶等式理论的公理最小化问题。已有工作表明，对群、布尔代数等一阶等式理论，同调方法可给出公理数量下界。作者将这一结果推广到高阶情形：考虑带积类型和单位类型的简单类型λ演算，研究λ项之间等式构成的集合。论文定义给定等式理论的同调群，并证明可由这些同调群计算该理论所需等式数量的下界。结果属于理论层面的贡献，未涉及实现或实验评估。
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.