License
when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.235
URN: urn:nbn:de:0030-drops-31208
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3120/

Moser, Georg ; Schnabl, Andreas

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

pdf-format:
Dokument 1.pdf (565 KB)


Abstract

We study the complexity of rewrite systems shown terminating via the dependency pair framework using processors for reduction pairs, dependency graphs, or the subterm criterion. The complexity of such systems is bounded by a multiple recursive function, provided the complexity induced by the employed base techniques is at most multiple recursive. Moreover this upper bound is tight.

BibTeX - Entry

@InProceedings{moser_et_al:LIPIcs:2011:3120,
  author =	{Georg Moser and Andreas Schnabl},
  title =	{{Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{235--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3120},
  URN =		{urn:nbn:de:0030-drops-31208},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.235},
  annote =	{Keywords: Complexity, DP Framework, Multiple Recursive Functions}
}

Keywords: Complexity, DP Framework, Multiple Recursive Functions
Seminar: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue date: 2011
Date of publication: 26.04.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI