Lower bounds for runtime complexity of term rewriting

DOI10.1007/S10817-016-9397-XMaRDI QIDQ2398176zbMATH OpenOpenAlexFDO

Authors Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, Thomas Ströder

Publication date 15 August 2017

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-016-9397-x

zbMATH Keywords

complexity analysisinductionlower boundsterm rewriting

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

Recommendations

• Inferring lower bounds for runtime complexity
• Complexity analysis for term rewriting by integer transition systems
• Analyzing runtime complexity via innermost runtime complexity
• Transforming derivational complexity of term rewriting to runtime complexity
• Lower runtime bounds for integer programs

Cites work

• A combination framework for complexity
• A theory of type polymorphism in programming
• Amortised resource analysis and typed polynomial interpretations
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automated Complexity Analysis Based on the Dependency Pair Method
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated termination analysis of Java bytecode by term rewriting
• Automatic Termination
• Finding and certifying loops
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 2090320 (Why is no real title available?)
• Inferring lower bounds for runtime complexity
• Johann Faulhaber and Sums of Powers
• Loop detection in term rewriting using the eliminating unfoldings
• Lower runtime bounds for integer programs
• Modular complexity analysis for term rewriting
• On the inference of resource usage upper and lower bounds
• Proving Non-looping Non-termination Automatically
• Proving termination by dependency pairs and inductive theorem proving
• Term Rewriting and All That
• Termination of string rewriting proved automatically
• Termination of term rewriting: Interpretation and type elimination
• Termination proofs and the length of derivations
• Termination proofs for string rewriting systems via inverse match-bounds
• The derivational complexity induced by the dependency pair method
• The undecidability of the Turing machine immortality problem

Cited in

(10)

• Constant runtime complexity of term rewriting is semi-decidable
• Transforming derivational complexity of term rewriting to runtime complexity
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Lower runtime bounds for integer programs
• Analyzing runtime complexity via innermost runtime complexity
• Inferring lower bounds for runtime complexity
• Analysing parallel complexity of term rewriting
• On complexity bounds and confluence of parallel term rewriting
• Data-driven runtime complexity analysis
• A dependency pair framework for relative termination of term rewriting

Describes a project that uses

Uses Software

• TcT
• z3
• Matchbox
• ML
• LoAT
• AProVE

This page was built for publication: Lower bounds for runtime complexity of term rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2398176)