Uncurrying for termination and complexity

DOI10.1007/S10817-012-9248-3zbMATH Open1286.68262OpenAlexW1983193642MaRDI QIDQ352959FDOQ352959

Authors: Nao Hirokawa, Aart Middeldorp, Harald Zankl 

Publication date: 5 July 2013

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

Full work available at URL: https://doi.org/10.1007/s10817-012-9248-3

Recommendations

• Uncurrying for Termination
• Generalized and formalized uncurrying
• Comparing curried and uncurried rewriting
• A termination ordering for higher order rewrite systems
• Termination proofs in the dependency pair framework May induce multiple recursive derivational complexity

zbMATH Keywords

term rewritingterminationuncurrying

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Termination of term rewriting using dependency pairs
• Joint spectral radius theory for automated complexity analysis of rewrite systems
• Satisfiability of non-linear (ir)rational arithmetic
• Complexity analysis of term rewriting based on matrix and context dependent interpretations
• Uncurrying for termination and complexity
• Automated Complexity Analysis Based on the Dependency Pair Method
• Title not available (Why is that?)
• Modular complexity analysis via relative complexity
• The Derivational Complexity Induced by the Dependency Pair Method
• Term Rewriting and All That
• Normalization results for typeable rewrite systems
• Some characteristics of strong innermost normalization
• Comparing curried and uncurried rewriting
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Automating the dependency pair method
• The simply typed rewriting calculus
• Generalized and formalized uncurrying
• HORPO with Computability Closure: A Reconstruction
• Polymorphic higher-order recursive path orderings
• Signature extensions preserve termination. An alternative proof via dependency pairs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Revisiting matrix interpretations for polynomial derivational complexity of term rewriting
• Higher order dependency pairs for algebraic functional systems
• Polynomially bounded matrix interpretations
• Random Descent
• Frontiers of Combining Systems
• Uncurrying for Termination
• Term Rewriting and Applications
• Logic for Programming, Artificial Intelligence, and Reasoning
• Rewriting Techniques and Applications
• Modular properties of conditional term rewriting systems
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting

Cited In (7)

• Comparing curried and uncurried rewriting
• A combination framework for complexity
• Uncurrying for termination and complexity
• Title not available (Why is that?)
• Uncurrying for Termination
• A Lambda-Free Higher-Order Recursive Path Order
• Generalized and formalized uncurrying

Uses Software

• Tyrolean

This page was built for publication: Uncurrying for termination and complexity

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