Recursive Path Orderings Can Also Be Incremental

In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering =B. It can be used for incremental (innermost) termination proofs of hierarchical unions by defining =B as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly.

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
• Keywords: LPAR 2005, Ordering =B, Recursive Path Ordering, Termination Proof