2021

  1. Star Games and Hydras
    Jörg Endrullis, Jan Willem Klop, and Roy Overbeek
    Log. Methods Comput. Sci. , 17 (2) (2021)
    paper

    Summary

    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.

    Bibtex

    @article{termination:star:games:2021,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Overbeek, Roy},
  title = {Star Games and Hydras},
  journal = {Log. Methods Comput. Sci.},
  volume = {17},
  number = {2},
  year = {2021},
  url = {https://lmcs.episciences.org/7518},
  biburl = {https://dblp.org/rec/journals/lmcs/EndrullisKO21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {journal}
}

    Digital Object Identifier

  2. Graph Rewriting and Relabeling with PBPO\(^\Mbox+\)
    Roy Overbeek, Jörg Endrullis, and RossetAloı̈s
    In: Graph Transformation - 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings Gadducci, Fabio and Kehrer, Timo (eds.) , pp. 60–80 , Springer (2021)
    paper

    Summary

    We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting with strong matching. Our approach, called PBPO+, exerts more control over the embedding of the pattern in the host graph, which is important for a large class of graph rewrite systems. In addition, we show that PBPO+ is well-suited for rewriting labeled graphs and certain classes of attributed graphs. For this purpose, we employ a lattice structure on the label set and use order-preserving graph morphisms. We argue that our approach is simpler and more general than related relabeling approaches in the literature.

    An extended version appeared as Graph rewriting and relabeling with PBPO+: A unifying theory for quasitoposes (JLAMP 2023).

    Bibtex

    @inproceedings{graph:rewriting:pbpo:2021,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg and Rosset, Alo{\"{\i}}s},
  editor = {Gadducci, Fabio and Kehrer, Timo},
  title = {Graph Rewriting and Relabeling with PBPO\({}^{\mbox{+}}\)},
  booktitle = {Graph Transformation - 14th International Conference, {ICGT} 2021,
                    Held as Part of {STAF} 2021, Virtual Event, June 24-25, 2021, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {12741},
  pages = {60--80},
  publisher = {Springer},
  year = {2021},
  url = {https://doi.org/10.1007/978-3-030-78946-6\_4},
  doi = {10.1007/978-3-030-78946-6\_4},
  biburl = {https://dblp.org/rec/conf/gg/OverbeekER21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-030-78946-6_4
  3. From Linear Term Rewriting to Graph Rewriting with Preservation Of Termination
    Roy Overbeek, and Jörg Endrullis
    In: Proceedings Twelfth International Workshop on Graph Computational Models, GCM@STAF 2021, Online, 22nd June 2021 Hoffmann, Berthold and Minas, Mark (eds.) , pp. 19–34 (2021)
    paper

    Summary

    Encodings of term rewriting systems (TRSs) into graph rewriting systems usually lose global termination, meaning the encodings do not terminate on all graphs. A typical encoding of the terminating TRS rule a(b(x)) -> b(a(x)), for example, may be indefinitely applicable along a cycle of a's and b's. Recently, we introduced PBPO+, a graph rewriting formalism in which rules employ a type graph to specify transformations and control rule applicability. In the present paper, we show that PBPO+ allows for a natural encoding of linear TRS rules that preserves termination globally. This result is a step towards modeling other rewriting formalisms, such as lambda calculus and higher order rewriting, using graph rewriting in a way that preserves properties like termination and confluence. We moreover expect that the encoding can serve as a guide for lifting TRS termination methods to PBPO+ rewriting.

    Bibtex

    @inproceedings{graph:termination:linear:2021,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  editor = {Hoffmann, Berthold and Minas, Mark},
  title = {From Linear Term Rewriting to Graph Rewriting with Preservation of
                    Termination},
  booktitle = {Proceedings Twelfth International Workshop on Graph Computational
                    Models, GCM@STAF 2021, Online, 22nd June 2021},
  series = {{EPTCS}},
  volume = {350},
  pages = {19--34},
  year = {2021},
  url = {https://doi.org/10.4204/EPTCS.350.2},
  doi = {10.4204/EPTCS.350.2},
  biburl = {https://dblp.org/rec/journals/corr/abs-2106-13826.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {workshop}
}

    Digital Object Identifier

    10.4204/EPTCS.350.2