Document Open Access Logo

Hydra Battles and AC Termination

Authors Nao Hirokawa , Aart Middeldorp

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.12.pdf
  • Filesize: 0.73 MB
  • 16 pages

Document Identifiers

Author Details

Nao Hirokawa
  • School of Information Science, JAIST, Ishikawa, Japan
Aart Middeldorp
  • Department of Computer Science, Universität Innsbruck, Austria

Funding

  • Hirokawa, Nao: JSPS KAKENHI Grant Number JP22K11900.
  • Middeldorp, Aart: Part of this work was performed when the second author was employed at the Future Value Creation Research Center of Nagoya University, Japan.

Cite AsGet BibTex

Nao Hirokawa and Aart Middeldorp. Hydra Battles and AC Termination. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.12

Abstract

We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Rewrite systems
  • Theory of computation → Computability
Keywords
  • battle of Hercules and Hydra
  • term rewriting
  • termination

Metrics

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

References

  1. Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas, and Rafael Navarro-Marset. Proving termination properties with MU-TERM. In Proc. 13th Algebraic Methodology and Software Technology, volume 6486 of Lecture Notes in Computer Science, pages 201-208, 2011. URL: https://doi.org/10.1007/978-3-642-17796-5_12.
  2. Wilfried Buchholz. An independence result for (π₁¹ - CA) + BI. Annals of Pure and Applied Logic, 33:131-155, 1987. URL: https://doi.org/10.1016/0168-0072(87)90078-9.
  3. Wilfried Buchholz. Another rewrite system for the standard Hydra battle. In Proc. Mini-Workshop: Logic, Combinatorics and Independence Results, volume 3(4) of Oberwolfach Reports, pages 3099-3102. European Mathematical Society, 2006. Google Scholar
  4. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems. Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243-320. Elsevier, 1990. Google Scholar
  5. Nachum Dershowitz and Georg Moser. The Hydra battle revisited. In Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, volume 4600 of Lecture Notes in Computer Science, pages 1-27, 2007. URL: https://doi.org/10.1007/978-3-540-73147-4_1.
  6. Jörg Endrullis, Jan Willem Klop, and Roy Overbeek. Star games and Hydras. Logical Methods in Computer Science, 17(2):20:1-20:32, 2021. URL: https://doi.org/10.23638/LMCS-17(2:20)2021.
  7. Maria C. F. Ferreira and Hans Zantema. Total termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing, 7(2):133-162, 1996. URL: https://doi.org/10.1007/BF01191381.
  8. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning, 58(1):3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  9. Nao Hirokawa and Aart Middeldorp. Hydra battles and AC termination. In Proc. 18th International Workshop on Termination, pages 21-25, 2022. Google Scholar
  10. Dieter Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science, 105(1):129-140, 1992. URL: https://doi.org/10.1016/0304-3975(92)90289-R.
  11. Laurence Kirby and Jeff Paris. Accessible independency results for Peano arithmetic. Bulletin of the London Mathematical Society, 14:285-325, 1982. URL: https://doi.org/10.1112/blms/14.4.285.
  12. Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Proc. 20th International Conference on Rewriting Techniques and Applications, volume 5595 of Lecture Notes in Computer Science, pages 295-304, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_21.
  13. Ingo Lepper. Derivation lengths and order types of Knuth-Bendix orders. Theoretical Computer Science, 269(1-2):433-450, 2001. URL: https://doi.org/10.1016/S0304-3975(01)00015-9.
  14. Ingo Lepper. Simply terminating rewrite systems with long derivations. Archive for Mathematical Logic, 43(1):1-18, 2004. URL: https://doi.org/10.1007/s00153-003-0190-2.
  15. Aart Middeldorp and Hitoshi Ohsaki. Type introduction for equational rewriting. Acta Informatica, 36(12):1007-1029, 2000. URL: https://doi.org/10.1007/PL00013300.
  16. Aart Middeldorp and Hans Zantema. Simple termination of rewrite systems. Theoretical Computer Science, 175(1):127-158, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00172-7.
  17. Georg Moser. The Hydra battle and Cichon’s principle. Applicable Algebra in Engineering, Communication and Computing, 20(2):133-158, 2009. URL: https://doi.org/10.1007/s00200-009-0094-4.
  18. Georg Moser and Andreas Schnabl. The derivational complexity induced by the dependency pair method. Logical Methods in Computer Science, 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:1)2011.
  19. Hitoshi Ohsaki, Aart Middeldorp, and Jürgen Giesl. Equational termination by semantic labelling. In Proc. 14th EACSL Annual Conference on Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 457-471, 2000. URL: https://doi.org/10.1007/3-540-44622-2_31.
  20. Albert Rubio. A fully syntactic AC-RPO. Information and Computation, 178(2):515-533, 2002. URL: https://doi.org/10.1006/inco.2002.3158.
  21. Hélène Touzet. Encoding the Hydra battle as a rewrite system. In Proc. 23rd International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 267-276, 1998. URL: https://doi.org/10.1007/BFb0055776.
  22. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Nagoya termination tool. In Proc. 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science, pages 466-475, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_32.
  23. Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp. AC-KBO revisited. Theory and Practice of Logic Programming, 16(2):163-188, 2016. URL: https://doi.org/10.1017/S1471068415000083.
  24. Harald Zankl, Sarah Winkler, and Aart Middeldorp. Beyond polynomials and Peano arithmetic - Automation of elementary and ordinal interpretations. Journal of Symbolic Computation, 69:129-158, 2015. URL: https://doi.org/10.1016/j.jsc.2014.09.033.
  25. Hans Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17(1):23-50, 1994. URL: https://doi.org/10.1006/jsco.1994.1003.
  26. Hans Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89-105, 1995. URL: https://doi.org/10.3233/FI-1995-24124.
  27. Hans Zantema. The termination hierarchy for term rewriting. Applicable Algebra in Engineering, Communication and Computing, 12(1-2):3-19, 2001. URL: https://doi.org/10.1007/s002000100061.
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