The Hydra Battle and Cichon’s Principle

Georg Moser

Applicable Algebra in Engineering, Communication and Computing 20(2), pp. 133 – 158, 2009.


In rewriting the Hydra battle refers to a term rewrite system H proposed by Dershowitz and Jouannaud. To date, H withstands any attempt to prove its termination automatically. This motivates our interest in term rewrite systems encoding the Hydra battle, as a careful study of such systems may prove useful in the design of automatic termination tools. Moreover it has been an open problem, whether any termination order compatible with H has to have the Howard-Bachmann ordinal as its order type, i.e., the proof theoretic ordinal of the theory of one inductive definition. We answer this question in the negative, by providing a reduction order compatible with H, whose order is at most epsilon_0, the proof theoretic ordinal of Peano arithmetic.


  PDF |    doi:10.1007/s00200-009-0094-4 |  © Springer


author = "Georg Moser",
title = "The {H}ydra {B}attle and {C}ichon's {P}rinciple",
journal = "Applicable Algebra in Engineering, Communication and Computing",
volume = 20,
number = 2,
year = 2009,
pages = "133--158"
Nach oben scrollen