Star games and hydras

Jörg Endrullis; Jan Willem Klop; Roy Overbeek

doi:10.23638/LMCS-17(2:20)2021

Star games and hydras

Jörg Endrullis, Jan Willem Klop, Roy Overbeek

Research output: Contribution to Journal › Article › Academic › peer-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 language	English
Article number	20
Pages (from-to)	1-32
Number of pages	32
Journal	Logical Methods in Computer Science
Volume	17
Issue number	2
Early online date	27 May 2021
DOIs	https://doi.org/10.23638/LMCS-17(2:20)2021
Publication status	Published - 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

Access to Document

10.23638/LMCS-17(2:20)2021

Handle.net

Persistent link

Cite this

@article{fe27c4a902c8497d938a4859c9fbbe97,

title = "Star games and hydras",

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 {\textquoteleft}star{\textquoteright} 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.",

keywords = "Buchholz Hydra, Hydra battle, Iterative path ordering, Kruskal{\textquoteright}s tree theorem, Recursive path ordering, Termination, Well-quasi-ordering",

author = "J{\"o}rg Endrullis and Klop, {Jan Willem} and Roy Overbeek",

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: {\textcopyright} J{\"o}rg Endrullis, Jan Willem Klop, and Roy Overbeek.",

year = "2021",

doi = "10.23638/LMCS-17(2:20)2021",

language = "English",

volume = "17",

pages = "1--32",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "2",

}

TY - JOUR

T1 - Star games and hydras

AU - Endrullis, Jörg

AU - Klop, Jan Willem

AU - Overbeek, Roy

N1 - 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.

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

KW - Buchholz Hydra

KW - Hydra battle

KW - Iterative path ordering

KW - Kruskal’s tree theorem

KW - Recursive path ordering

KW - Termination

KW - Well-quasi-ordering

UR - http://www.scopus.com/inward/record.url?scp=85118150857&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85118150857&partnerID=8YFLogxK

U2 - 10.23638/LMCS-17(2:20)2021

DO - 10.23638/LMCS-17(2:20)2021

M3 - Article

AN - SCOPUS:85118150857

VL - 17

SP - 1

EP - 32

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 20

ER -

Star games and hydras

Abstract

Bibliographical note

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Cite this