Jörg Endrullis ; Jan Willem Klop ; Roy Overbeek - Star Games and Hydras

lmcs:6056 - Logical Methods in Computer Science, May 27, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:20)2021
Star Games and HydrasArticle

Authors: Jörg Endrullis ; Jan Willem Klop ; Roy Overbeek

    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.


    Volume: Volume 17, Issue 2
    Published on: May 27, 2021
    Accepted on: March 11, 2021
    Submitted on: January 27, 2020
    Keywords: Computer Science - Logic in Computer Science

    Classifications

    Consultation statistics

    This page has been seen 1707 times.
    This article's PDF has been downloaded 309 times.