CeTA

Introduction

For the paper Generalized and Formalized Uncurrying we have run two sets of experiments. All experiments have been performed on a machine with 8 Dual Core AMD Opteron 885 processors and 64GB RAM running Linux.

The first set has been run on the 195 ATRSs of the TPDB (the same problem set as for the paper "Uncurrying for Termination"). The timeout was 10 seconds and we used the following DP processors for proving termination:

subterm criterion - The well known subterm criterion.
matrix (dimension 1) - The reduction pair processor with usable rules, using matrix interpretations of dimension one.
matrix (dimension 2) - The reduction pair processor with usable rules, using matrix interpretations of dimension two.

Concerning uncurrying we used the following approaches:

none No uncurrying.
trs Try to uncurry once and for all, before switching from the given TRS to the initial DP problem.
U'₁ Generalized uncurrying in the DP framework.
U'₂ Generalized uncurrying in the DP framework with special treatment of tuple symbols.

The second set has been run on the 511 TRSs that remained after using the July 2010 competition strategy (restricted to certifiable techniques) of TTT2 on the TPDB version 8.0 (excluding any SRSs). The timeout was 5 seconds and we used the following heuristics for computing the applicative arities:

π₊ Use the maximal occurring applicative arity.
π_± Similar to π₊, but the arities are decreased such that eta-expansion is not required.
π_- Use the minimal occurring applicative arity (reducing the number of uncurrying rules).

Interesting examples

In the following examples uncurrying has been applied successfully, although none of these examples is applicative.