Matrix Interpretations on Polyhedral Domains

7 years 10 months ago
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
Johannes Waldmann
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where RTA
Authors Johannes Waldmann
Comments (0)