Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874110 | Information Processing Letters | 2018 | 6 Pages |
Abstract
We prove that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be examined by considering finitely many start terms. We implemented our semi-decision procedure in the tool AProVE to show its efficiency and its success for systems where state-of-the-art complexity analysis tools fail.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Florian Frohn, Jürgen Giesl,