| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jürgen Giesl and Hans Zantema
Date: July 2010
Summary: Can we use the dependency pair method to prove relative termination?
The key of the success of the dependency pair method in proving termination is the following property from [AG00, GTSKF06], stated in more recent terminology:
A TRS R is terminating if and only if the dependency pair problem (DP(R),R) is terminating.
A dependency pair problem is a pair (P,R) of TRSs. Such a dependency pair problem is called terminating if it admits no infinite chain, that is, there is no P ∪ R reduction containing infinitely many P-steps, where P-steps only occur at the root.
Can we use the dependency pair method to prove relative termination? Here for a pair (R,S) of TRSs, R is said to be terminating modulo S if there is no R ∪ S reduction containing infinitely many R-steps. This is the same requirement as for termination of a dependency pair problem, except that the first TRS in a dependency pair problem may only be used for root steps. So, more precisely, the open problem is:
Find a “useful” effectively computable function φ from pairs of TRSs to dependency pair problems, such that for every two TRSs R,S the TRS R is terminating modulo S if and only if the dependency pair problem φ(R,S) is terminating.
Here, “useful” means that the resulting dependency pair problem φ(R,S) should be “easy” (i.e., suitable for automated termination analysis by existing tools).
| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |