Homological Invariants of Higher-Order Equational Theories
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917367042277376 |
|---|---|
| author | Ikebuchi, Mirai |
| author_facet | Ikebuchi, Mirai |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_10149 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Homological Invariants of Higher-Order Equational Theories Ikebuchi, Mirai Logic in Computer Science Category Theory Logic 03G30 F.4.1 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. |
| title | Homological Invariants of Higher-Order Equational Theories |
| topic | Logic in Computer Science Category Theory Logic 03G30 F.4.1 |
| url | https://arxiv.org/abs/2505.10149 |