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.

翻译：我们提出了一种新的赫拉克勒斯与九头蛇之战的重写系统编码，该系统包含AC符号。与早期的项重写编码不同，该编码忠实地模拟了赫拉克勒斯击败九头蛇的任何策略。为证明我们编码的终止性，我们采用了类型引入与针对AC重写的多类语义标记相结合的方法，并引入AC-MPO——一种全新的AC可兼容归约序，可视为AC-RPO的弱化版本。