Generating polynomial orderings (Q1318775): Difference between revisions

From MaRDI portal
Set OpenAlex properties.
Import recommendations run Q6767936
 
(One intermediate revision by one other user not shown)
Property / cites work
 
Property / cites work: Termination of rewriting systems by polynomial interpretations and its implementation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4079613 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A note on simplification orderings / rank
 
Normal rank
Property / cites work
 
Property / cites work: Termination of rewriting / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automating the Knuth Bendix ordering / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5812325 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Termination proofs and the length of derivations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5581665 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3779786 / rank
 
Normal rank
Property / Recommended article
 
Property / Recommended article: Generating polynomial orderings for termination proofs / rank
 
Normal rank
Property / Recommended article: Generating polynomial orderings for termination proofs / qualifier
 
Similarity Score: 0.88000464
Amount0.88000464
Unit1
Property / Recommended article: Generating polynomial orderings for termination proofs / qualifier
 
Property / Recommended article
 
Property / Recommended article: Polynomials and operator orderings / rank
 
Normal rank
Property / Recommended article: Polynomials and operator orderings / qualifier
 
Similarity Score: 0.8770711
Amount0.8770711
Unit1
Property / Recommended article: Polynomials and operator orderings / qualifier
 
Property / Recommended article
 
Property / Recommended article: Q3708893 / rank
 
Normal rank
Property / Recommended article: Q3708893 / qualifier
 
Similarity Score: 0.8768228
Amount0.8768228
Unit1
Property / Recommended article: Q3708893 / qualifier
 
Property / Recommended article
 
Property / Recommended article: Polynomial Path Orders / rank
 
Normal rank
Property / Recommended article: Polynomial Path Orders / qualifier
 
Similarity Score: 0.87470317
Amount0.87470317
Unit1
Property / Recommended article: Polynomial Path Orders / qualifier
 
Property / Recommended article
 
Property / Recommended article: Polynomials over ordered fields / rank
 
Normal rank
Property / Recommended article: Polynomials over ordered fields / qualifier
 
Similarity Score: 0.86692154
Amount0.86692154
Unit1
Property / Recommended article: Polynomials over ordered fields / qualifier
 
Property / Recommended article
 
Property / Recommended article: Order polynomials and Pólya's enumeration theorem. / rank
 
Normal rank
Property / Recommended article: Order polynomials and Pólya's enumeration theorem. / qualifier
 
Similarity Score: 0.86341095
Amount0.86341095
Unit1
Property / Recommended article: Order polynomials and Pólya's enumeration theorem. / qualifier
 
Property / Recommended article
 
Property / Recommended article: Query order in the polynomial hierarchy / rank
 
Normal rank
Property / Recommended article: Query order in the polynomial hierarchy / qualifier
 
Similarity Score: 0.85653
Amount0.85653
Unit1
Property / Recommended article: Query order in the polynomial hierarchy / qualifier
 
Property / Recommended article
 
Property / Recommended article: Combinatorial polar orderings and recursively orderable arrangements / rank
 
Normal rank
Property / Recommended article: Combinatorial polar orderings and recursively orderable arrangements / qualifier
 
Similarity Score: 0.85441923
Amount0.85441923
Unit1
Property / Recommended article: Combinatorial polar orderings and recursively orderable arrangements / qualifier
 
Property / Recommended article
 
Property / Recommended article: Q4520757 / rank
 
Normal rank
Property / Recommended article: Q4520757 / qualifier
 
Similarity Score: 0.8507766
Amount0.8507766
Unit1
Property / Recommended article: Q4520757 / qualifier
 
Property / Recommended article
 
Property / Recommended article: A generalized ordered Bell polynomial / rank
 
Normal rank
Property / Recommended article: A generalized ordered Bell polynomial / qualifier
 
Similarity Score: 0.85010433
Amount0.85010433
Unit1
Property / Recommended article: A generalized ordered Bell polynomial / qualifier
 

Latest revision as of 11:52, 4 April 2025

scientific article
Language Label Description Also known as
English
Generating polynomial orderings
scientific article

    Statements

    Generating polynomial orderings (English)
    0 references
    0 references
    4 April 1994
    0 references
    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 the binary logarithmic function to these products. We have implemented a prototype of this algorithm. The implementation does not require any user interactions. Note that the technique is not a decision procedure (because of the approximation). However, it is very useful in practice as confirmed by the following statistics: We have applied the algorithm to 242 TRSs occurring in the literature (which are all orientable with the help of simple-mixed polynomials). For 228 TRSs (94.2 \%) the method was successful.
    0 references
    simplification orderings
    0 references
    polynomial orderings
    0 references
    term rewriting systems
    0 references
    termination
    0 references
    reduction orderings
    0 references
    simplex method
    0 references

    Identifiers