Campus Event Calendar
Event Entry
What and Who
Complexity Analysis for Term Rewriting by Integer Transition Systems
Florian Frohn
RWTH Aachen
Talk
AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 24 January 2019
16:00
60 Minutes
E1 5
002
Saarbrücken
Abstract
While programs operating on integers are akin to integer
transition systems (ITSs), programs operating on data structures
can be transformed to term rewrite systems (TRSs) in many
cases. In the last years, powerful complexity analysis techniques
for ITSs have been developed. To make them available for the
analysis of programs operating on data structures, we present a
suitable transformation from TRSs to ITSs. It first uses a novel
sufficient criterion to prove that, independently of the
evaluation strategy under consideration, the complexity of the
analyzed TRS is bounded by its complexity w.r.t. eager
evaluation. Next, the TRS is transformed into a recursive program
over the natural numbers. As ITSs are restricted to tail
recursion, we then show how to analyze the resulting recursive
program iteratively. In each iteration, a tail-recursive function
is analyzed by existing complexity analysis tools for ITSs. Then,
calls to this function are eliminated, so that non-tail-recursive
program parts become tail-recursive and can be analyzed in the
next iteration.
transition systems (ITSs), programs operating on data structures
can be transformed to term rewrite systems (TRSs) in many
cases. In the last years, powerful complexity analysis techniques
for ITSs have been developed. To make them available for the
analysis of programs operating on data structures, we present a
suitable transformation from TRSs to ITSs. It first uses a novel
sufficient criterion to prove that, independently of the
evaluation strategy under consideration, the complexity of the
analyzed TRS is bounded by its complexity w.r.t. eager
evaluation. Next, the TRS is transformed into a recursive program
over the natural numbers. As ITSs are restricted to tail
recursion, we then show how to analyze the resulting recursive
program iteratively. In each iteration, a tail-recursive function
is analyzed by existing complexity analysis tools for ITSs. Then,
calls to this function are eliminated, so that non-tail-recursive
program parts become tail-recursive and can be analyzed in the
next iteration.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/21/2019 09:04 -- Created document.