Information Technology Reference
In-Depth Information
Table 1.
Negative constants: termination.
constant
0
,
1
0
,
1
,
2
0
,
1
, −
1
coecient
0
,
1
0
,
1
,
2
0
,
1
interpretation
e
n
ne
e
n
ne
e
n
ne
success
179
158
182
180
159
183
188
164
191
0.20
0.09
0.08
0.20
0.09
0.09
0.24
0.14
0.12
failure
40
61
37
39
60
36
31
55
28
0.03
0.02
0.03
1.11
0.15
1.43
0.93
0.43
1.29
ti
eo t
0
0
0
0
0
0
0
0
0
total time
36.41 15.72 16.56
78.48 23.88 67.29
73.01 46.14 59.45
Table 2.
Negative constants: innermost termination.
constant
0
,
1
0
,
1
,
2
0
,
1
, −
1
coecient
0
,
1
0
,
1
,
2
0
,
1
interpretation
e
n
ne
e
n
ne
e
n
ne
success
200
177
202
202
179
204
209
183
211
0.19
0.10
0.09
0.19
0.10
0.09
0.23
0.14
0.12
failure
39
62
37
37
60
35
30
56
28
0.04
0.03
0.05
1.19
0.16
1.47
0.92
0.43
1.26
ti
eo t
0
0
0
0
0
0
0
0
0
total time
39.46 18.92 19.59
81.94 26.97 70.07
75.24 49.10 61.24
with
a
1
,...,a
n
in the indicated coecient range and
b
in the indicated constant
e
range. In the columns labelled
we do not fix the interpretations in advance; for
all function symbols we search for an appropriate linear interpretation. In the
columns labelled
ne
we start with the default natural interpretations but allow
other linear interpretations if (innermost) termination cannot be proved. Deter-
mining appropriate coecients can be done by a straightforward but inecient
“generate and test” algorithm. We implemented a more involved algorithm in
our termination tool, but we anticipate that the recent techniques described in
[6] might be useful to optimize the search for coecients.
We list the number of successful termination attempts, the number of failures
(which means that no termination proof was found while fully exploring the
search space implied by the options), and the number of timeouts, which we set
to 30 seconds. The figures below the number of successes and failures indicate
the average time in seconds.
Search WWH ::
Custom Search