Report on the use of polynomials with real and rational coefficients in proofs of termination

Author

Salvador Lucas

Abstract

After its introduction in the late seventies, the use of polynomial orderings in proofs of termination decayed in favour of syntactic path orderings like RPO. Recent developments, however, have brought new applications for them. Most implementations only consider polynomial interpretations with integer coefficients. We have recently proved that real or rational coefficients can also be helpful. In this paper we summarize our research in this area.

Keywords

Polynomial orderings, program analysis, term rewriting, termination.