General remarks
The experiments mentioned below were done with the tpdb-4.0, which
can be obtained
here. We have conducted tests
single-threaded on a server equipped with 8 AMD Opteron 2.8 GHz dual core processors
with 64GB of RAM, and on a 2.40 GHz Intel Core 2 Duo with 2 GB of memory.
For the experiments, we used the tool TCT, which is an extension of the termination
prover TTT2. A binary of TCT (native compiled OCaml) can be obtained
here.
The following abbreviations are used for the test results:
- YES (Y) means that a polynomial derivational complexity proof has been found
- MAYBE (M) means that no proof could be found
- TIMEOUT (T) means that the timeout limit of 60 seconds has been reached before
a proof has been found or the search for a proof was finished
- - means that an error occurred: either the given system specified a non-standard
reduction strategy or theory or was a relative termination example, or an
internal error (e.g. stack overflow) occurred
The following strategies have been tested in the table below:
- SLI: strongly linear polynomial interpretations (equivalent to triangular matrix
interpretations of dimension 1). In TCT, this method is used by typing e.g.
./tct -p -s '(natinter -i -c stronglylinear -b 63)[60]' <TRS>,
which searches for SLIs with coefficients up to 63, with a timeout of 60 seconds.
- Match-bounds: This method (taken from TTT2)
is called by typing
./tct -p -s 'if duplicating then fail else bound' <TRS>.
Note that all methods described here can be caused to fast-fail by preceding
the argument of the -s flag by if duplicating then fail else.
- CDI: delta-restricted context-dependent interpretations. In TCT,
this can be done by typing e.g.
./tct -p -s '(natinter -i -c deltarestricted -b 15)[60]' <TRS>,
which searches for a delta-restricted interpretation with coefficients at most 15.
- TMI: triangular matrix interpretations. This can be applied in
TCT by typing e.g.
./tct -p -s '(minter -i -c triangular -b 15 -d 2)[60]' <TRS>,
which searches for a 2-dimensional triangular matrix interpretation with coefficients at most 15.
- TMI+Matchbounds: combination of the two methods, as described in the paper.
In TCT, this combination can be achieved
by typing e.g.
./tct -p -s 'if duplicating then fail else
((minter -i -c triangular -b 15 -d 2)[30] | bound)[60]' <TRS>.
In all cases, we immediately returned "MAYBE" if the given system was duplicating,
because it is impossible that the system has polynomial derivational complexity in
that case.
The following table gives an overview of the experimental results
(tables created with a modified version of a privately communicated script by Nao Hirokawa):
Summary results for SLI, match-bounds and CDI
Individual results
| status |
SLI |
MATCHBOUNDS |
CDI_DRES_A |
CDI_DRES_B |
CDI_DRES_C |
CDI_DRES_D |
| YES |
41 |
125 |
42 |
83 |
85 |
86 |
| total time |
1.43 |
89.46 |
101.45 |
322.64 |
318.33 |
374.16 |
| avg. time |
0.03 |
0.72 |
2.42 |
3.89 |
3.75 |
4.35 |
| MAYBE |
1338 |
928 |
1236 |
1126 |
1069 |
1022 |
| total time |
132.76 |
32.94 |
1591.12 |
2120.20 |
1931.42 |
1272.84 |
| avg. time |
0.10 |
0.04 |
1.29 |
1.88 |
1.81 |
1.25 |
| TIMEOUT |
2 |
328 |
103 |
172 |
227 |
272 |
| total time |
120.04 |
19686.40 |
6186.58 |
10330.05 |
13633.01 |
16335.91 |
| avg. time |
60.02 |
60.02 |
60.06 |
60.06 |
60.06 |
60.06 |
Summary for triangular matrix interpretations (dimension2)
Individual results
| status |
MINTER_TRI_B_A |
MINTER_TRI_B_B |
MINTER_TRI_B_C |
MINTER_TRI_B_D |
| YES |
80 |
134 |
143 |
143 |
| total time |
3.12 |
19.72 |
35.62 |
36.90 |
| avg. time |
0.04 |
0.15 |
0.25 |
0.26 |
| MAYBE |
1301 |
1245 |
1216 |
1159 |
| total time |
54.52 |
240.17 |
1277.64 |
1942.85 |
| avg. time |
0.04 |
0.19 |
1.05 |
1.68 |
| TIMEOUT |
0 |
2 |
22 |
79 |
| total time |
0.00 |
120.05 |
1320.45 |
4741.68 |
| avg. time |
0.00 |
60.02 |
60.02 |
60.02 |
Summary for triangular matrix interpretations (dimension3)
Individual results
| status |
MINTER_TRI_C_A |
MINTER_TRI_C_B |
MINTER_TRI_C_C |
MINTER_TRI_C_D |
| YES |
126 |
152 |
157 |
156 |
| total time |
8.12 |
147.73 |
220.14 |
165.70 |
| avg. time |
0.06 |
0.97 |
1.40 |
1.06 |
| MAYBE |
1253 |
1141 |
1034 |
1000 |
| total time |
226.34 |
1928.02 |
1100.73 |
421.91 |
| avg. time |
0.18 |
1.69 |
1.06 |
0.42 |
| TIMEOUT |
2 |
88 |
190 |
225 |
| total time |
120.05 |
5282.01 |
11404.50 |
13505.23 |
| avg. time |
60.02 |
60.02 |
60.02 |
60.02 |
Summary for triangular matrix interpretations (dimension4)
Individual results
| status |
MINTER_TRI_D_A |
MINTER_TRI_D_B |
MINTER_TRI_D_C |
MINTER_TRI_D_D |
| YES |
131 |
150 |
152 |
153 |
| total time |
73.61 |
128.55 |
97.35 |
148.33 |
| avg. time |
0.56 |
0.86 |
0.64 |
0.97 |
| MAYBE |
1215 |
1039 |
992 |
986 |
| total time |
1372.79 |
1123.78 |
360.86 |
389.12 |
| avg. time |
1.13 |
1.08 |
0.36 |
0.39 |
| TIMEOUT |
35 |
192 |
237 |
242 |
| total time |
2100.77 |
11524.67 |
14225.90 |
14526.05 |
| avg. time |
60.02 |
60.02 |
60.02 |
60.03 |
Summary for triangular matrix interpretations (dimension5)
Individual results
| status |
MINTER_TRI_E_A |
MINTER_TRI_E_B |
MINTER_TRI_E_C |
MINTER_TRI_E_D |
| YES |
134 |
149 |
152 |
152 |
| total time |
123.20 |
169.25 |
219.06 |
232.86 |
| avg. time |
0.92 |
1.14 |
1.44 |
1.53 |
| MAYBE |
1136 |
1010 |
985 |
980 |
| total time |
1442.56 |
576.01 |
394.26 |
425.03 |
| avg. time |
1.27 |
0.57 |
0.40 |
0.43 |
| TIMEOUT |
111 |
222 |
244 |
249 |
| total time |
6662.54 |
13325.75 |
14646.56 |
14946.54 |
| avg. time |
60.02 |
60.03 |
60.03 |
60.03 |
Summary for the combination of triangular MI and match-bounds
Individual results
| status |
MI_MB_TRI_B_D |
MI_MB_TRI_C_D |
MI_MB_TRI_D_D |
MI_MB_TRI_E_D |
| YES |
210 |
216 |
214 |
212 |
| total time |
909.95 |
1860.43 |
1878.68 |
1923.87 |
| avg. time |
4.33 |
8.61 |
8.78 |
9.07 |
| MAYBE |
928 |
928 |
928 |
928 |
| total time |
32.85 |
33.09 |
32.52 |
32.34 |
| avg. time |
0.04 |
0.04 |
0.04 |
0.03 |
| TIMEOUT |
243 |
237 |
239 |
241 |
| total time |
14585.20 |
14225.21 |
14345.47 |
14465.60 |
| avg. time |
60.02 |
60.02 |
60.02 |
60.02 |