Orderings for Innermost Termination

Abstract. This paper shows that the suitable orderings for proving innermost termination are characterized by the innermost parallel monotonicity, IP-monotonicity for short. This property may lead to several innermost-specific orderings. Here, an IP-monotonic version of the Recursive Path Ordering is presented. This variant can be used (directly or as ingredient of the Dependency Pairs method) for proving innermost termination of non-terminating term rewrite systems.

• Type: Conference
• Year: 2005
• Where: RTA
• Authors: Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
• Keywords: Innermost Parallel Monotonicity, Innermost Termination, Recursive Path Ordering, RTA 2005, Theoretical Computer Science