Polynomially Bounded Matrix Interpretations

Matrix interpretations can be used to bound the derivational complexity of rewrite systems. We present a criterion that completely characterizes matrix interpretations that are polynomially bounded. It includes the method of upper triangular interpretations as a special case, and we prove that the inclusion is strict. The criterion can be expressed as a finite domain constraint system. It translates to a Boolean constraint system with a size that is polynomial in the dimension of the interpretation. We report on performance of an implementation.

• Type: Conference
• Year: 2010
• Where: RTA
• Authors: Johannes Waldmann
• Keywords: Domain Constraint System, Matrix Interpretations, RTA 2010, Theoretical Computer Science, Upper Triangular Interpretations