Document Open Access Logo

Polynomial Termination Over ℕ Is Undecidable

Authors Fabian Mitterwallner , Aart Middeldorp

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.27.pdf
  • Filesize: 0.74 MB
  • 17 pages

Document Identifiers

Author Details

Fabian Mitterwallner
  • Department of Computer Science, Universität Innsbruck, Austria
Aart Middeldorp
  • Department of Computer Science, Universiät Innsbruck, Austria
  • Future Value Creation Research Center, Nagoya University, Japan

Cite AsGet BibTex

Fabian Mitterwallner and Aart Middeldorp. Polynomial Termination Over ℕ Is Undecidable. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.27

Abstract

In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Rewrite systems
  • Theory of computation → Computability
Keywords
  • Term Rewriting
  • Polynomial Termination
  • Undecidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  3. Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137-159, 1987. URL: https://doi.org/10.1016/0167-6423(87)90030-X.
  4. 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.
  5. Jörg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of rewrite systems. Journal of Automated Reasoning, 40(2-3):195-220, 2008. URL: https://doi.org/10.1007/s10817-007-9087-9.
  6. Alfons Geser. Relative Termination. PhD thesis, University of Passau, Germany, 1990. URL: https://doi.org/10.18725/OPARU-2427.
  7. David Hilbert. Mathematical problems. Bulletin of the American Mathematical Society, 8(10):437-479, 1902. URL: https://doi.org/10.1090/S0002-9904-1902-00923-3.
  8. Dieter Hofbauer and Clemens Lautemann. Termination proofs and the length of derivations (preliminary version). In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 167-177, 1989. URL: https://doi.org/10.1007/3-540-51081-8_107.
  9. Adam Koprowski and Johannes Waldmann. Max/plus tree automata for termination of term rewriting. Acta Cybernetica, 19(2):357-392, 2009. Google Scholar
  10. Dallas Lankford. On proving term rewrite systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA, 1979. Google Scholar
  11. Salvador Lucas. On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Applicable Algebra in Engineering, Communication and Computing, 17(1):49-73, 2006. URL: https://doi.org/10.1007/s00200-005-0189-5.
  12. Yuri Y. Matijasevic. Enumerable sets are diophantine (translated from Russian). In Soviet Mathematics Doklady, volume 11, pages 354-358, 1970. Google Scholar
  13. Aart Middeldorp, Hitoshi Ohsaki, and Hans Zantema. Transforming termination by self-labelling. In Proceedings of the 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Artificial Intelligence, pages 373-387, 1996. URL: https://doi.org/10.1007/3-540-61511-3_101.
  14. Fabian Mitterwallner and Aart Middeldorp. Polynomial termination over N is undecidable. In Samir Genaim, editor, Proceedings of the 17th International Workshop on Termination, pages 21-26, 2021. Google Scholar
  15. Friedrich Neurauter and Aart Middeldorp. Polynomial interpretations over the natural, rational and real numbers revisited. Logical Methods in Computer Science, 10(3:22):1-28, 2014. URL: https://doi.org/10.2168/LMCS-10(3:22)2014.
  16. Christian Sternagel and Aart Middeldorp. Root-labeling. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 336-350, 2008. URL: https://doi.org/10.1007/978-3-540-70590-1_23.
  17. Hans Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89-105, 1995. URL: https://doi.org/10.3233/FI-1995-24124.
  18. Hans Zantema. Termination. In Term Rewriting Systems, chapter 6, pages 181-259. Cambridge University Press, 2003. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact