On recursive path ordering

DOI10.1016/0304-3975(85)90175-6MaRDI QIDQ1082075zbMATH OpenOpenAlexFDO

Authors Mukkai S. Krishnamoorthy, Paliath Narendran

Publication date 1985

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(85)90175-6

zbMATH Keywords

term rewriting systemsterminationwell-founded partial order

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Review text

The recursive path ordering (RPO) scheme of Dershowitz is a powerful way of extending a partial order on a set of function symbols to a well- founded partial order on their set of terms. We prove that, given a pair of terms, the problem of deciding whether they can be made RPO- comparable, by choosing a partial order on their function symbols, is NP- complete.

Recommendations

• Maximal extensions of simplification orderings
• Practical algorithms for deciding path ordering constraint satisfaction.
• scientific article; zbMATH DE number 3905845
• scientific article; zbMATH DE number 3921961
• The recursive path and polynomial ordering for first-order and higher-order terms

Cites work

• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• scientific article; zbMATH DE number 3810909 (Why is no real title available?)
• scientific article; zbMATH DE number 3905845 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• On Proving Uniform Termination and Restricted Termination of Rewriting Systems
• Orderings for term-rewriting systems

Cited in

(28)

• Simplification orderings: Putting them to the test
• Practical algorithms for deciding path ordering constraint satisfaction.
• Orienting rewrite rules with the Knuth-Bendix order.
• An improved general path order
• SAT solving for termination proofs with recursive path orders and dependency pairs
• How to sort by walking and swapping on paths and trees
• The size-change principle and dependency pairs for termination of term rewriting
• Maximal extensions of simplification orderings
• A Lambda-Free Higher-Order Recursive Path Order
• The computability path ordering
• The Computability Path Ordering: The End of a Quest
• Polymorphic higher-order recursive path orderings
• scientific article; zbMATH DE number 3921961 (Why is no real title available?)
• scientific article; zbMATH DE number 1223728 (Why is no real title available?)
• scientific article; zbMATH DE number 1342225 (Why is no real title available?)
• scientific article; zbMATH DE number 1104447 (Why is no real title available?)
• AC-KBO revisited
• scientific article; zbMATH DE number 1405624 (Why is no real title available?)
• Open problems in rewriting
• Recursive Path Orderings Can Also Be Incremental
• Quasi-interpretations. A way to control resources
• Proving Termination with (Boolean) Satisfaction
• A Higher-Order Iterative Path Ordering
• Iterative Lexicographic Path Orders
• Improving associative path orderings
• On the complexity of recursive path orderings
• Inferring RPO symbol orderings
• Termination of string rewriting proved automatically

Describes a project that uses

Uses Software

• REVE
• RRL

This page was built for publication: On recursive path ordering

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