2026-07-23T22:06:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1762 2024-03-06T10:33:05Z ddc:004 open_access

Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations Moser, Georg Schnabl, Andreas Waldmann, Johannes Term Rewriting Derivational Complexity Termination Automation For a given (terminating) term rewriting system one can often estimate its \emph{derivational complexity} indirectly by looking at the proof method that established termination. In this spirit we investigate two instances of the interpretation method: \emph{matrix interpretations} and \emph{context dependent interpretations}. We introduce a subclass of matrix interpretations, denoted as \emph{triangular matrix interpretations}, which induce polynomial derivational complexity and establish tight correspondence results between a subclass of context dependent interpretations and restricted triangular matrix interpretations. The thus obtained new results are easy to implement and considerably extend the analytic power of existing results. We provide ample numerical data for assessing the viability of the method. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Georg Moser and Andreas Schnabl and Johannes Waldmann 2008 Is Part Of LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2008.1762 urn:nbn:de:0030-drops-17626 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1762 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode