Recursive Decomposition Ordering and Multiset Orderings
The Recursive Decomposition Ordering, a simplification ordering on terms, is useful to prove termination of term rewriting systems. In this paper we give the definition of the decomposition ordering and prove that it is a well-founded simplication ordering containing Dershowitz's Recursive Path...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149029 |
| Summary: | The Recursive Decomposition Ordering, a simplification ordering on terms, is useful to prove termination of term rewriting systems. In this paper we give the definition of the decomposition ordering and prove that it is a well-founded simplication ordering containing Dershowitz's Recursive Path Ordering. We also show that the Recursive Decomposition Ordering has a very interesting incremental property. In the second paper, we propose two well-founded orderings on multisets that extend the Dershowitz-Manna ordering. Unlike the Dershowitz-Manna ordering, ours do not have a natural monotonicity property. This lack of monotonicity suggests using monotonicity to provide a new characterization of the Dershowitz -Manna ordering. Section 5 proposes an efficient and correct implementation of that ordering. |
|---|