[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #23 (Solved !)

Originator: E. A. Cichon [Cic90]
Date: April 1991

Summary: Must any termination ordering used for proving termination of the Battle of Hydra and Hercules-system have the Howard ordinal as its order type?

The following system [DJ90], based on the “Battle of Hydra and Hercules” in [KP82], is terminating, but not provably so in Peano Arithmetic:

h(z,e(x))→h(c(z),d(z,x))
d(z,g(0,0))→e(0)
d(z,g(x,y))→g(e(x),d(z,y))
d(c(z),g(g(x,y),0))→g(d(c(z),g(x,y)),d(z,g(x,y)))
g(e(x),e(y))→e(g(x,y))

Transfinite (є0-) induction is required for a proof of termination. Must any termination ordering have the Howard ordinal as its order type, as conjectured in [Cic90]?

Remark

If the notion of termination ordering is formalized by using ordinal notations with variables, then a termination proof using such orderings yields a slow growing bound on the lengths of derivations. If the order type is less than the Howard-Bachmann ordinal then, by Girard’s Hierarchy Theorem, the derivation lengths are provably total in Peano Arithmetic. Hence a termination proof for this particular rewrite system for the Hydra game cannot be given by such an ordering [Andreas Weiermann, personal communication].

Remark

This has been answered to the negative by Georg Moser [Mos09], by giving a reduction order that is compatible with the above rewrite system, and whose order type is at most є0 (the proof theoretic ordinal of Peano arithmetic).

References

[Cic90]
E. A. Cichon. Bounds on derivation lengths from termination proofs. Technical Report CSD-TR-622, Department of Computer Science, University of London, Surrey, England, June 1990.
[DJ90]
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.
[KP82]
Laurie Kirby and Jeff Paris. Accessible independence results for Peano arithmetic. Bulletin London Mathematical Society, 14:285–293, 1982.
[Mos09]
Georg Moser. The Hydra battle and Cichon’s principle. Applicable Algebra in Engineering, Communication and Computing, 20(2):133–158, 2009. doi:10.1007/s00200-009-0094-4.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]