Matrix Interpretations on Polyhedral Domains

We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds, and we discuss its relation with the usable rules criterion. We present an implementation and experiments. 1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs Keywords and phrases Termination of term rewriting, matrix interpretations, constraint programming, linear inequalities Digital Object Identifier 10.4230/LIPIcs.RTA.2015.318

• Type: Journal
• Year: 2015
• Where: RTA
• Authors: Johannes Waldmann
• Keywords: RTA 2015, Theoretical Computer Science