RISC Forum

Symbolic constraints arising in proofs of termination of programs are often translated into numeric constraints before checking them for satisfiability. In this setting, polynomial interpretations are a simple and popular choice. Elementary functions, where not only addition and product but also exponential, fractional, and trigonometric expressions are allowed, provide a natural extension of polynomial functions. Although the use of elementary algebraic interpretations in proofs of termination of term rewriting was proposed more than ten years ago, the automatic generation of such interpretations for a given program was an open problem. This is an important drawback for using these interpretations in practice. We show how to solve this problem by using a combination of rewriting, CLP, and CSP techniques for handling the elementary constraints which are obtained when giving parametric elementary interpretations to the symbols. We believe that the solution which we propose for this particular case study can be easily generalized to deal with more general numeric algebras. Thus, it can be thought as a first step towards a generic framework for using numeric algebras in automatic proofs of termination.