Applications of Homological Algebra to Equational Theories

It is well-known that some equational theories such as groups or Boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting system), using homological algebra. Their method is an analog of Squier’s homology theory on string rewriting systems. In this dissertation, I develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. Also, the same methodology applies to equational unification, the problem of solving an equation modulo equational axioms. I provide a relationship between equational unification and homological algebra for equational theories. I will construct abelian groups associated with equational theories. Then, the main theorem gives a necessary condition of equational unifiability that is described in terms of the abelian groups and homomorphisms between them.

Name thesis:degree_name

Doctoral

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2022

Author dc:creator

• Ikebuchi, Mirai

Advisor dc:contributor.advisor

• Chlipala, Adam

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright MIT

Licence dc:rights.uri

• http://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/143377

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/143377