License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.09411.5
URN: urn:nbn:de:0030-drops-24233
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2423/
Go to the corresponding Portal

Fuhs, Carsten ; Giesl, Jürgen ; Plücker, Martin ; Schneider-Kamp, Peter ; Falke, Stephan

Termination of Integer Term Rewriting

pdf-format:
09411.GieslJuergen.ExtAbstract.2423.pdf (0.09 MB)

Abstract

Recently, techniques and tools from term rewriting have been successfully applied to prove termination automatically for different programming languages. The advantage of rewrite techniques is that they are very powerful for algorithms on user-defined data structures. But in contrast to techniques for termination analysis of imperative programs, the drawback of rewrite techniques is that they do not support data structures like integer numbers which are pre-defined in almost all programming languages.

To solve this problem, we extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term
rewriting automatically. Our experiments show that this indeed combines the power of rewrite techniques on user-defined data types with a powerful treatment of pre-defined integers.

BibTeX - Entry

@InProceedings{fuhs_et_al:DagSemProc.09411.5,
  author =	{Fuhs, Carsten and Giesl, J\"{u}rgen and Pl\"{u}cker, Martin and Schneider-Kamp, Peter and Falke, Stephan},
  title =	{{Termination of Integer Term Rewriting}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2423},
  URN =		{urn:nbn:de:0030-drops-24233},
  doi =		{10.4230/DagSemProc.09411.5},
  annote =	{Keywords: Termination analysis, integers, term rewriting, dependency pairs}
}

Keywords: Termination analysis, integers, term rewriting, dependency pairs
Collection: 09411 - Interaction versus Automation: The two Faces of Deduction
Issue Date: 2010
Date of publication: 09.03.2010

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