TcT 2.0 on Resource Aware ML

This test illustrates the gain in power when using the decompose, dependency pairs and dependency graph decomposition processors.

Testbed

As testbed we use a straight forward translations of Resource aware ML programs to TRSs. The main purpose of this automatic transformation is to produce interesting examples of considerable sizes. Intentionally no effort was put into making the resulting TRSs easier to analyse. This generated testbed can be downloaded from here.
To reflect the evaluation strategy of the RaML input program, we assess the innermost runtime complexity of the TRSs obtained from the translation.

Setup

All experiments were performed on a machine with 8 dual core AMD Opteron(tm) 885 processors @ 2.60GHz processors and 16Gb of RAM. The experiments were generated using following TcT configuration resulting in this x86_64 binary. Employed strategies are recorded in the test file.

Applied Techniques

On these pages we contrast following techniques:

• semantic methods:
  With this test we check the power of semantical methods employed directly on the input TRS, which clearly illustrates the need for transformations. As processors we used matrix interpretations of dimension one to four, as well as polynomial interpretations, run in parallel.
• decompose:
  In this test we indicate the strength of Zankl and Korps modular approach as described in Modular Complexity Analysis via Relative Complexity. Here we have used their central (de)composition processor in combination with semantical methods as above. Although experimental data shows that this method improves the power of semantical methods, still a majority of the example TRSs cannot be handled.
• DP + decompose:
  In this test we proceed as above, but we first apply the weak dependency pair (in case the weightgap condition can be established), respectively dependency tuples transformation. We direct the semantic methods toward orienting leafs in the dependency graph, so that these can be dropped from the dependency problem. Also, we employ various simplifications, usable rules for instance. Compare our framework paper.
  This test indicates the usefulness of the dependency pair transformations. Two additional problems can be solved in the dependency pair setting, and for one problem a more precise certificate could be obtained. Still, a majority of the problems remain open. The search space on these reasonable sized problems is simply too high, TcT fails to synthesise proper interpretations.
• DP + DG decompose:
  This test indicates the strengh of our new dependency graph decomposition processor. Here we first transform the input problem into a depenency pair problem (DP problem for short). To avoid imprecision of the certificate, we try to solve the resulting problem as in the test decompose. Only when this approach gets stuck, we decompose the dependency graph (DG for short) by separating topmost cycles from the DP problem. This procedure gets repeated until all cycles are eventually solved.
  The experimental data shows the gain in power through this modular approach. A clear drawback of this method however is that DG decomposition might overestimate the complexity. In order to retain a precise complexity certificate, we are forced to apply this method only as a last means, which results in signifficantly higher execution times.
• DP + DG decompose (greedy):
  This final test is as above, with the exception that dependency graph decomposition is exhaustively applied directly after the dependency pair transformation.
  In comparison to the previous test, we see a signifficant increase in speed, at the cost of precision of the obtained complexity certificate.

Experimental Results

Overview

Average Execution Time (in seconds)

Details

Results are also available as a Prolog database.