Homological Invariants of Higher-Order Equational Theories

TL;DR

This paper extends homological methods to analyze higher-order equational theories, providing a way to estimate the minimal number of axioms needed using homology groups.

Contribution

It introduces a homological framework for higher-order theories, generalizing previous first-order results to simply typed lambda calculus.

Findings

Homology groups can be computed for higher-order equational theories.

Lower bounds on the number of equations are derived from homology groups.

The approach applies to theories with lambda calculus, product, and unit types.

Abstract

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.