A Homological Condition on Equational Unifiability

Ikebuchi, Mirai

doi:10.4230/LIPIcs.MFCS.2021.61

File

LIPIcs.MFCS.2021.61.pdf

Filesize: 0.73 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.MFCS.2021.61
URN: urn:nbn:de:0030-drops-145010

Author Details

Mirai Ikebuchi

Massachuseetts Institute of Technology, Cambridge, MA, USA

Acknowledgements

I would like to thank Assaf Kfoury and Keisuke Nakano for reading a draft of this paper and for their helpful suggestions.

Cite AsGet BibTex

Mirai Ikebuchi. A Homological Condition on Equational Unifiability. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 61:1-61:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.61

Abstract

Equational unification is the problem of solving an equation modulo equational axioms. In this paper, we provide a relationship between equational unification and homological algebra for equational theories. We will construct a functor from the category of sets of equational axioms to the category of abelian groups. Then, our main theorem gives a necessary condition of equational unifiability that is described in terms of abelian groups associated with equational axioms and homomorphisms between them. To construct our functor, we use a ringoid (a category enriched over the category of abelian groups) obtained from the equational axioms and a free resolution of a "good" module over the ringoid, which was developed by Malbos and Mimram.

Subject Classification

ACM Subject Classification

Theory of computation → Equational logic and rewriting

Keywords

Equational unification
Homological algebra
equational theories

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

María Alpuente, Santiago Escobar, and José Iborra. Termination of narrowing revisited. Theoretical Computer Science, 410(46):4608-4625, 2009. Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi.
Franz Baader, Wayne Snyder, Paliath Narendran, Manfred Schmidt-Schauss, and Klaus Schulz. Unification theory. In Handbook of Automated Reasoning, Handbook of Automated Reasoning, pages 445-533. North-Holland, Amsterdam, 2001.
K. S. Brown. Cohomology of Groups, volume 87 of Graduate Texts in Mathematics. Springer-Verlag New York, 1982.
W. Brown. Matrices over commutative rings. M. Dekker, New York, 1993.
Martin Davis. Hilbert’s tenth problem is unsolvable. The American Mathematical Monthly, 80(3):233-269, 1973. URL: https://doi.org/10.1080/00029890.1973.11993265.
M. Fay. First-order unification in an equational theory. In 4th Workshop on Automated Deduction, Austin, Texas, 1978.
Jean-Marie Hullot. Canonical forms and unification. In Wolfgang Bibel and Robert Kowalski, editors, 5th Conference on Automated Deduction Les Arcs, France, July 8-11, 1980, pages 318-334, Berlin, Heidelberg, 1980. Springer Berlin Heidelberg.
Mirai Ikebuchi. A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:17, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
M. Jantzen. A note on a special one-rule semi-thue system. Information Processing Letters, 21(3):135-140, 1985.
Mamuka Jibladze and Teimuraz Pirashvili. Cohomology of algebraic theories. Journal of Algebra, 137(2):253-296, 1991.
P. Malbos and S. Mimram. Homological computations for term rewriting systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Ju V Matijasevic. Enumerable sets are diophantine. In Soviet Math. Dokl., volume 11, pages 354-358, 1970.
B. Mitchell. Rings with several objects. Advances in Mathematics, 8(1):1-161, 1972.
C. C. Squier. Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra, 49(1-2):201-217, 1987.
Charles A. Weibel. An Introduction to Homological Algebra. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1994.