[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

## Problem #106

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 PR 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 RS 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).

## References

[AG00]
Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
[GTSKF06]
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. Mechanizing and improving dependency pairs. Journal of Automated Reasoning, 37(3):155–203, 2006.

 [Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]