Star games and hydras

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

The recursive path ordering is an established and crucial tool in term rewriting to prove termination. We revisit its presentation by means of some simple rules on trees (or corresponding terms) equipped with a ‘star’ as control symbol, signifying a command to make that tree (or term) smaller in the order being defined. This leads to star games that are very convenient for proving termination of many rewriting tasks. For instance, using already the simplest star game on finite unlabeled trees, we obtain a very direct proof of termination of the famous Hydra battle, direct in the sense that there is not the usual mention of ordinals. We also include an alternative road to setting up the star games, using a proof method of Buchholz, adapted by van Oostrom, resulting in a quantitative version of the star as control symbol. We conclude with a number of questions and future research directions.

Original languageEnglish
Article number20
Pages (from-to)1-32
Number of pages32
JournalLogical Methods in Computer Science
Volume17
Issue number2
Early online date27 May 2021
DOIs
Publication statusPublished - 2021

Bibliographical note

Funding Information:
We thank Nachum Dershowitz for his useful conversations concerning a draft of this paper and many comments and pointers to the literature, during his sabbatical period at CWI Amsterdam around end of 2019 and beginning of 2020. Also we gratefully acknowledge support for our research from CWI Amsterdam and the Section Theory of the Vrije Universiteit Amsterdam. The third author received funding from NWO under the Innovational Research Incentives Scheme (project No. VI.Vidi.192.004). The second author is thankful for monthly funding from the Dutch ABP, the Algemeen Burgerlijk Pensioenfonds, for daily subsistence and cost of living.

Publisher Copyright:
© Jörg Endrullis, Jan Willem Klop, and Roy Overbeek.

Keywords

  • Buchholz Hydra
  • Hydra battle
  • Iterative path ordering
  • Kruskal’s tree theorem
  • Recursive path ordering
  • Termination
  • Well-quasi-ordering

Fingerprint

Dive into the research topics of 'Star games and hydras'. Together they form a unique fingerprint.

Cite this