Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp

TL;DR
This paper introduces a novel encoding of the Hercules and Hydra battle problem as an AC rewrite system, accurately modeling strategies and proving termination using advanced rewriting techniques.
Contribution
It presents a new encoding that faithfully models Hercules' strategies and introduces AC-MPO, a weakened AC-compatible reduction order for termination proofs.
Findings
Encoding faithfully models Hercules' strategies
AC-MPO is effective for termination proofs
Employs type introduction and semantic labeling techniques
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-MPO, a new AC compatible reduction order that can be seen as a much weakened version of AC-RPO.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Digital and Cyber Forensics · Security and Verification in Computing
