Lower bounds for runtime complexity of term rewriting

DOI10.1007/s10817-016-9397-xzbMath1409.68254OpenAlexW2561310305MaRDI QIDQ2398176

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

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

lower boundsinductionterm rewritingcomplexity analysis

Mathematics Subject Classification ID

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

Related Items (3)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Analysing parallel complexity of term rewriting ⋮ Constant runtime complexity of term rewriting is semi-decidable

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Proving termination by dependency pairs and inductive theorem proving
• Termination of string rewriting proved automatically
• Termination proofs for string rewriting systems via inverse match-bounds
• Loop detection in term rewriting using the eliminating unfoldings
• A theory of type polymorphism in programming
• Termination of term rewriting: Interpretation and type elimination
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Lower Runtime Bounds for Integer Programs
• Proving Non-looping Non-termination Automatically
• On the Inference of Resource Usage Upper and Lower Bounds
• A Combination Framework for Complexity
• Johann Faulhaber and Sums of Powers
• Finding and Certifying Loops
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated Complexity Analysis Based on the Dependency Pair Method
• Automatic Termination
• Term Rewriting and All That
• Termination proofs and the length of derivations
• Amortised Resource Analysis and Typed Polynomial Interpretations
• Inferring Lower Bounds for Runtime Complexity
• Automated Termination Analysis of Java Bytecode by Term Rewriting
• Modular Complexity Analysis for Term Rewriting
• Frontiers of Combining Systems
• The undecidability of the Turing machine immortality problem
• The Derivational Complexity Induced by the Dependency Pair Method

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