License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.12
URN: urn:nbn:de:0030-drops-179965
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17996/
Go to the corresponding LIPIcs Volume Portal

Hirokawa, Nao ; Middeldorp, Aart

Hydra Battles and AC Termination

pdf-format:
LIPIcs-FSCD-2023-12.pdf (0.7 MB)

Abstract

We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.

BibTeX - Entry

@InProceedings{hirokawa_et_al:LIPIcs.FSCD.2023.12,
  author =	{Hirokawa, Nao and Middeldorp, Aart},
  title =	{{Hydra Battles and AC Termination}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17996},
  URN =		{urn:nbn:de:0030-drops-179965},
  doi =		{10.4230/LIPIcs.FSCD.2023.12},
  annote =	{Keywords: battle of Hercules and Hydra, term rewriting, termination}
}

Keywords: battle of Hercules and Hydra, term rewriting, termination
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI