Document Open Access Logo

A Homological Condition on Equational Unifiability

Author Mirai Ikebuchi

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2021.61.pdf
  • Filesize: 0.73 MB
  • 16 pages

Document Identifiers

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

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.

Cite As Get 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

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.

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. K. S. Brown. Cohomology of Groups, volume 87 of Graduate Texts in Mathematics. Springer-Verlag New York, 1982. Google Scholar
  4. W. Brown. Matrices over commutative rings. M. Dekker, New York, 1993. Google Scholar
  5. 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.
  6. M. Fay. First-order unification in an equational theory. In 4th Workshop on Automated Deduction, Austin, Texas, 1978. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. M. Jantzen. A note on a special one-rule semi-thue system. Information Processing Letters, 21(3):135-140, 1985. Google Scholar
  10. Mamuka Jibladze and Teimuraz Pirashvili. Cohomology of algebraic theories. Journal of Algebra, 137(2):253-296, 1991. Google Scholar
  11. 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. Google Scholar
  12. Ju V Matijasevic. Enumerable sets are diophantine. In Soviet Math. Dokl., volume 11, pages 354-358, 1970. Google Scholar
  13. B. Mitchell. Rings with several objects. Advances in Mathematics, 8(1):1-161, 1972. Google Scholar
  14. C. C. Squier. Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra, 49(1-2):201-217, 1987. Google Scholar
  15. Charles A. Weibel. An Introduction to Homological Algebra. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact