Star Games and Hydras
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) smal...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6056/pdf |
| _version_ | 1797268551417987072 |
|---|---|
| author | Jörg Endrullis Jan Willem Klop Roy Overbeek |
| author_facet | Jörg Endrullis Jan Willem Klop Roy Overbeek |
| author_sort | Jörg Endrullis |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:17Z |
| format | Article |
| id | doaj.art-399e96b540cf48d2a89d224daee6d6df |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:17Z |
| publishDate | 2021-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-399e96b540cf48d2a89d224daee6d6df2024-03-08T10:33:57ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-05-01Volume 17, Issue 210.23638/LMCS-17(2:20)20216056Star Games and HydrasJörg EndrullisJan Willem KlopRoy OverbeekThe 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.https://lmcs.episciences.org/6056/pdfcomputer science - logic in computer science |
| spellingShingle | Jörg Endrullis Jan Willem Klop Roy Overbeek Star Games and Hydras Logical Methods in Computer Science computer science - logic in computer science |
| title | Star Games and Hydras |
| title_full | Star Games and Hydras |
| title_fullStr | Star Games and Hydras |
| title_full_unstemmed | Star Games and Hydras |
| title_short | Star Games and Hydras |
| title_sort | star games and hydras |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/6056/pdf |
| work_keys_str_mv | AT jorgendrullis stargamesandhydras AT janwillemklop stargamesandhydras AT royoverbeek stargamesandhydras |