Nao Hirokawa, Aart Middeldorp
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 22:1-12:16, 2023.
pdf 
doi: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.
BibTex
@inproceedings{NHAM-FSCD23, author = "Nao Hirokawa and Aart Middeldorp", title = "Hydra Battles and {AC} Termination", booktitle = "Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction", editor = "Marco Gaboardi and Femke van Raamsdonk", series = "Leibniz International Proceedings in Informatics", volume = 260, pages = "12:1--12:16", year = 2023, doi = "10.4230/LIPIcs.FSCD.2023.12"}