Matrix Interpretations for Proving Termination of Term Rewriting |
| |
Authors: | Jörg Endrullis Johannes Waldmann Hans Zantema |
| |
Affiliation: | (1) Department of Computer Science, Vrije Universiteit Amsterdam, De Boelelaan 1081, 1081 HV Amsterdam, The Netherlands;(2) Hochschule für Technik, Wirtschaft und Kultur (FH) Leipzig, Fb IMN, PF 30 11 66, 04251 Leipzig, Germany;(3) Department of Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands |
| |
Abstract: | We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation
of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers,
ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by
matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict
steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding
the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean
satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. |
| |
Keywords: | Term rewriting Termination Matrix interpretations Satisfiability |
本文献已被 SpringerLink 等数据库收录! |
|