Goal directed and relative dependency pairs for the termination of narrowing

Jose Iborra, Naoki Nishida and German Vidal

Empirical evaluation

In the paper Goal-Directed and Relative Dependency Pairs for the Termination of Narrowing, we discuss a new approach to the automated proof of termination for narrowing from an initial goal. Instead of computing a global argument filtering which eliminates all the occurrences of logic variables, the proposed approach uses a framework of goal-directed dependency pairs with a specialized notion of usable rules, together with a novel result for relative termination proofs using dependency pairs. As a result it is no longer required to employ heuristics and search due to the implicit incompleteness of a global argument filtering, as it was the case in previous approaches.

Tools

In these experiments we compare our implementation of the new approach with a variant of the global filtering approach.

LOPSTR'09

The implementation of the approach described in the paper, using a reduction pair processor based on SAT solving complemented with a set of graph refinement processors: instantiation, forward instantiation and narrowing.

FLOPS'08 innermost

A variant of the global filtering approach described in Termination of Narrowing in Left-Linear Constructor Systems . Although this approach does not consider extra variables, our implementation replaces them with generators, in the spirit of the related work such as this paper or Automated Termination Analysis for Logic Programs by Term Rewriting. In order to compute safe argument filterins we use a simple innermost heuristic which selects always the innermost position. We also tried a search heuristic, based on generation of all the possible candidates and ranking based on the size of the right hand sides of pairs in the filtered problem, but this proved to work badly in practice. In order to ensure we compare apples to apples, the generated rewriting problems are solved using the same processors used in the LOPSTR09 implementation, together with a subterm criterion processor. We include the subterm criterion processor as a testament of the shortcomings created by the loss of minimality in the new approach, where such a processor cannot be used.

SGST'07 type

A variant of the global filtering approach described in Automated Termination Analysis for Logic Programs by Term Rewriting targeted at infinitary rewriting termination. As heuristic for selecting the optimal argument filterings, we use the advanced type heuristic described here . As above, the generated rewriting problems are solved using the same processors used in the LOPSTR09 implementation, together with a subterm criterion processor. We include the subterm criterion processor to exemplify the shortcomings created by the loss of minimality in the new approach, where such a processor cannot be used.

Examples

Web interface

Experiments

Summary:

Results::