Hydra Battles and AC Termination

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.