2025/05/15 by Mirai Ikebuchi, Ikebuchi, Mirai · 1 citation
Mathematics · Physics and Astronomy · #03G30 #Advanced Topics in Algebra #Algebraic structures and combinatorial models #Category Theory (math.CT) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Nonlinear Waves and Solitons
paper · doi:10.48550/arxiv.2505.10149
openalex publication_date 2025/05/15 · openalex created_date 2025/10/15 · openalex updated_date 2026/07/28
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.