Proving termination of (conditional) rewrite systems. A semantic approach
type: Item
instance of: scholarly article
title: Proving termination of (conditional) rewrite systems. A semantic approach
zbMATH Open document ID: 0790.68054
DOI: 10.1007/BF01209624
author: Eddy Bevers
author: Johan Lewi
published in: Acta Informatica
publication date: 1994-05-10T00:00:00Z
review text: An important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a rewrite system \(R\), do not suffice for proving termination of \(R\). Indeed sometimes semantic information is needed to orient a rewrite rule. Therefore we integrate a semantic interpretation of rewrite systems and terms into a well-founded ordering on terms: the notion of semantic ordering is the first main contribution of this paper. The use and usefulness of the semantic ordering in proving termination is illustrated by means of some realistic examples. Furthermore, the concept of semantic information induces a novel approach for proving termination in conditional rewrite systems. The idea is to employ not only semantic information contained in the terms that are to be compared, but also extra (semantic) information contained in the premiss of the conditional equation in which the terms appear. This leads to our second contribution in the termination problem area: the notion of contextual ordering and contextual semantic ordering. The contextual approach allows to prove termination of conditional rewrite systems where all classical partial orderings would fail.
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 567287
zbMATH Keywords: term rewriting
zbMATH Keywords: termination
zbMATH Keywords: semantic ordering
zbMATH Keywords: semantic information
zbMATH Keywords: conditional rewrite systems
zbMATH Keywords: contextual ordering
describes a project that uses: REVE
MaRDI profile type: Publication
cites work: Q3484358
cites work: Q3783521
cites work: Q3809306
cites work: Q3757390
cites work: Q3783523
cites work: Termination of rewriting systems by polynomial interpretations and its implementation
cites work: Conditional rewrite rules: Confluence and termination
cites work: Q3894958
cites work: Proving Properties of Programs by Structural Induction
cites work: Q3819993
cites work: A note on simplification orderings
cites work: Orderings for term-rewriting systems
cites work: Termination of rewriting
cites work: Rewriting techniques and applications. 3rd international conference, RTA-89, Chapel Hill, NC, USA, April 3--5, 1989. Proceedings
cites work: Q4385532
cites work: Q3659124
cites work: Conditional rewrite rules
cites work: Simplifying conditional term rewriting systems: Unification, termination and confluence
cites work: Q3683533
cites work: Q5581665
cites work: Q3336681
cites work: On the recursive decomposition ordering with lexicographical status and other related orderings
cites work: Q3779786
cites work: Q3696501
cites work: Q3805961
full work available at URL: https://doi.org/10.1007/bf01209624
OpenAlex ID: W2911610589
description: scientific article; zbMATH DE number 567287