Generating polynomial orderings
type: Item
instance of: scholarly article
title: Generating polynomial orderings
zbMATH Open document ID: 0791.68092
DOI: 10.1016/0020-0190(94)90032-9
author: Joachim Steinbach
published in: Information Processing Letters
publication date: 1994-04-04T00:00:00Z
review text: More and more, term rewriting systems (TRSs) are applied in computer science as well as in mathematics. They are based on directed equations which may be used as non-deterministic functional programs. Termination is a key property for computing with TRSs. There are various methods of proving termination of TRSs. Most of these are based on reduction orderings, which are well-founded, compatible with the structure of terms and stable with respect to substitutions. The notion of reduction ordering allows the following characterization of termination of TRSs: A TRS \({\mathcal R}\) terminates iff there exists a reduction ordering \(\succ\) such that \(l\succ r\) for each rule \(l\to r\) of \({\mathcal R}\). Polynomial orderings are special reduction orderings, mapping terms into a well-founded set by attaching monotonic polynomials (so- called interpretations) to operators. One of the main problems concerning polynomial orderings is the choice of adequate interpretations for a given TRS. The object of this paper is to describe an algorithm for finding polynomial interpretations for a given TRS. Based on the algorithm of U. Martin for generating an appropriate Knuth- Bendix ordering, we transform the set of rules into a set of linear inequalities based on the coefficients of the interpretations with respect to common monomials. The class of interpretations is restricted to so-called simple-mixed polynomials which are sufficient in practice. We make use of the simplex method for deciding whether a system of linear inequalities has a solution. Unfortunately, we do not have linear inequalities initially, because there might be sums of products resulting from strictly simple-mixed interpretations. In order to apply the simplex method we approximate more general inequalities to linear ones by (1) transforming the inequalities into inequalities, each side of which represents only one product (using a variant of the arithmetic-mean- geometric-mean inequality and by (2) applying…
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 540911
zbMATH Keywords: simplification orderings
zbMATH Keywords: polynomial orderings
zbMATH Keywords: term rewriting systems
zbMATH Keywords: termination
zbMATH Keywords: reduction orderings
zbMATH Keywords: simplex method
describes a project that uses: REVE
MaRDI profile type: Publication
full work available at URL: 0020-0190(94)90032-9
OpenAlex ID: W2038571924
cites work: Termination of rewriting systems by polynomial interpretations and its implementation
cites work: Q4079613
cites work: A note on simplification orderings
cites work: Termination of rewriting
cites work: Automating the Knuth Bendix ordering
cites work: Q5812325
cites work: Termination proofs and the length of derivations
cites work: Q5581665
cites work: Q3779786
Recommended article: Generating polynomial orderings for termination proofs
Recommended article: Polynomials and operator orderings
Recommended article: Q3708893
Recommended article: Polynomial path orders
Recommended article: Polynomials over ordered fields
Recommended article: Order polynomials and Pólya's enumeration theorem.
Recommended article: Query order in the polynomial hierarchy
Recommended article: Combinatorial polar orderings and recursively orderable arrangements
Recommended article: Q4520757
Recommended article: A generalized ordered Bell polynomial
description: scientific article; zbMATH DE number 540911