License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.329
URN: urn:nbn:de:0030-drops-31333
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3133/
Go to the corresponding LIPIcs Volume Portal

Sternagel, Christian ; Thiemann, René

Modular and Certified Semantic Labeling and Unlabeling

pdf-format:
26.pdf (0.6 MB)

Abstract

Semantic labeling is a powerful transformation technique to prove termination of term rewrite systems. The dual technique is unlabeling. For unlabeling it is essential to drop the so called decreasing rules which sometimes have to be added when applying semantic labeling. We indicate two problems concerning unlabeling and present our solutions.

The first problem is that currently unlabeling cannot be applied as a modular step, since the decreasing rules are determined by a semantic labeling step which may have taken place much earlier. To this end, we give an implicit definition of decreasing rules that does not depend on any knowledge about preceding labelings.

The second problem is that unlabeling is in general unsound. To solve this issue, we introduce the notion of extended termination problems. Moreover, we show how existing termination techniques can be lifted to operate on extended termination problems.

All our proofs have been formalized in Isabelle/HOL as part of the IsaFoR/CeTA project.

BibTeX - Entry

@InProceedings{sternagel_et_al:LIPIcs:2011:3133,
  author =	{Christian Sternagel and Ren{\'e} Thiemann},
  title =	{{Modular and Certified Semantic Labeling and Unlabeling}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{329--344},
  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/3133},
  URN =		{urn:nbn:de:0030-drops-31333},
  doi =		{10.4230/LIPIcs.RTA.2011.329},
  annote =	{Keywords: semantic labeling, certification, term rewriting, unlabeling}
}

Keywords: semantic labeling, certification, term rewriting, unlabeling
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

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